Thm* L:LangOver(Alph). Fin(Alph) Fin(x,y:Alph*//L-induced Equiv(x,y)) & (l:Alph*. Dec(L(l))) (St:Type, Auto:Automata(Alph;St). Fin(St) & L = LangOf(Auto)) mn_31

Thm* n:{1...}, A:Type, L:LangOver(A), R:(A*A*Prop). Fin(A) (EquivRel x,y:A*. x R y) (n ~ (x,y:A*//(x R y))) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))). l:A*. L(l) g(l)) (m:. m ~ (x,y:A*//(x L-induced Equiv y))) & (l:A*. Dec(L(l))) mn_23

Thm* L:LangOver(Alph), R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:Alph*//(x R y))). (l:Alph*. L(l) g(l)) x,y:Alph*//(x L-induced Equiv y) = x,y:Alph*//(x Rg y)) mn_23_Rl_equal_Rg

Thm* L:LangOver(Alph), R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) (g:((x,y:Alph*//(x R y))). l:Alph*. L(l) g(l)) & (x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))) (x,y:Alph*. (x R y) (x L-induced Equiv y)) mn_23_refinment

Thm* R:(A*A*Prop). (EquivRel x,y:A*. x R y) (x,y,z:A*. (x R y) ((z @ x) R (z @ y))) (g:((x,y:A*//(x R y))), L:LangOver(A). (l:A*. L(l) g(l)) (x,y:A*. (x L-induced Equiv y) (x Rg y))) Rl_iff_Rg

Thm* L:LangOver(A). EquivRel x,y:A*. x L-induced Equiv y lang_rel_equi

Thm* L:LangOver(A). Trans x,y:A*. x L-induced Equiv y lang_rel_tran

Thm* L:LangOver(A). Sym x,y:A*. x L-induced Equiv y lang_rel_symm

Thm* L:LangOver(A). Refl(A*;x,y.x L-induced Equiv y) lang_rel_refl