At: mn 13 1 1 2 1 1 1 1 1 1 1 1 1 1 2
1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. Fin(Alph)
5. Fin(St)
6. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
7. R: Alph*
Alph*Prop
8. EquivRel x,y:Alph*. x R y
9. g: (x,y:Alph*//R(x,y))
10. m: 
11. f: m(x,y:Alph*//R(x,y))
12. g1: (x,y:Alph*//R(x,y))m
13. InvFuns(m; x,y:Alph*//R(x,y); f; g1)
14. 
l:Alph*. LangOf(Auto)(l) 
g(l)
15. x,y,z:Alph*. R(x,y) 
R((z @ x),z @ y)
16. g1(nil) 
m
1
m
By: Analyze 16
Generated subgoals:None
About:
