Level: Lib Thy Top: 1 2
Hypotheses:- Alph :
- L : L(Alph)
- Fin(Alph)
- St :
- Auto : Automata(Alph;St)
- Fin(St)
- L = L(Auto)
- EquivRel(Alph List;x,y.Auto(x) = Auto(y))
Conclusion:
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: With 
x,y.Auto(x) = Auto(y)
(D 0)
Generated subgoals:1. (x,y.Auto(x) = Auto(y)) 
Alph List Alph List 2. EquivRel(Alph List;x,y.x (x,y.Auto(x) = Auto(y)) y)
c (g:x,y:(Alph List)//((x,y.Auto(x) = Auto(y)) x y)
Fin(x,y:(Alph List)//((x,y.Auto(x) = Auto(y)) x y))
(l:Alph List. L l (g l))
(x,y,z:Alph List.
(x,y.Auto(x) = Auto(y)) x y (x,y.Auto(x) = Auto(y)) (z @ x) (z @ y)))
3. 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)))