Level: Lib Thy Top:
Hypotheses:None
Conclusion:
Alph:
. L:L(Alph).
Fin(Alph)
(
St:. Auto:Automata(Alph;St). Fin(St) 
L = L(Auto))
(R:Alph List 
Alph List 
EquivRel(Alph List;x,y.x R y) c (g:x,y:(Alph List)//(R x y) 
Fin(x,y:(Alph List)//(R x y))
(l:Alph List. L l 
(g l))
(x,y,z:Alph List. R x y R (z @ x) (z @ y))))
Applied Tactic: UnivCD THENW Auto THEN D 4 THEN D 5 THEN D 6
Generated subgoals:1. R:Alph List Alph List
EquivRel(Alph List;x,y.x R y) c (g:x,y:(Alph List)//(R x y)
Fin(x,y:(Alph List)//(R x y))
(l:Alph List. L l (g l))
(x,y,z:Alph List. R x y R (z @ x) (z @ y)))