At: mn 12 1 2 3
1. Alph: Type
2. L: LangOver(Alph)
3. Fin(Alph)
4. St: Type
5. Auto: Automata(Alph;St)
6. Fin(St)
7. L = LangOf(Auto)
8. EquivRel x,y:Alph*. (Result(Auto)x) = (Result(Auto)y)
9. R: Alph*
Alph*Prop
(EquivRel x,y:Alph*. x R y) c
(
g:((x,y:Alph*//R(x,y))
).
Fin(x,y:Alph*//R(x,y))
& (
l:Alph*. L(l) 
g(l))
& (x,y,z:Alph*. R(x,y) 
R((z @ x),z @ y)))
Prop
By: Unfold `languages` 2
Generated subgoals:None
About:
