z:A*. 
(g(z@
x)) 
(g(z@y))
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* R:(Alph*Alph*Prop).
Fin(Alph)
(EquivRel x,y:Alph*. x R y)
Fin(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))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
mn_23_lem_1
Thm* R:(Alph*Alph*Prop).
Fin(Alph)
(EquivRel x,y:Alph*. x R y)
Fin(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))), x,y:x,y:Alph*//(x R y). Dec(x Rg y))
mn_23_lem
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* 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))). EquivRel u,v:x,y:A*//(x R y). u Rg v)
lquo_rel_equi
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))). Trans u,v:x,y:A*//(x R y). u Rg v)
lquo_rel_tran
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))). Sym u,v:x,y:A*//(x R y). u Rg v)
lquo_rel_symm
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))). Refl(x,y:A*//(x R y);u,v.u Rg v))
lquo_rel_refl