Level: Lib Thy Top: 1
Hypotheses:

  1. Alph :

  2. L : L(Alph)

  3. Fin(Alph)

  4. St :

  5. Auto : Automata(Alph;St)

  6. Fin(St)

  7. L = L(Auto)

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: Assert EquivRel(Alph List;x,y.Auto(x) = Auto(y))
Generated subgoals:

1. EquivRel(Alph List;x,y.Auto(x) = Auto(y))

2. 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)))