Alph:Type, L:LangOver(Alph). Fin(Alph) (St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto)) (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))))

1	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) 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)))

About: