At: mn 13 1 1 2 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. m ~ (x,y:Alph*//R(x,y))
12. 
l:Alph*. LangOf(Auto)(l) 
g(l)
13. x,y,z:Alph*. R(x,y) 
R((z @ x),z @ y)
g:((x,y:Alph*//(x R y))). l:Alph*. LangOf(Auto)(l) g(l)
By:
Witness g
THEN
Fold `languages` 0
Generated subgoals:None
About:
