At: mn 23 Rl equal Rg 1 5
1. Alph: Type
2. L: Alph*
Prop
3. R: Alph*Alph*Prop
4. EquivRel x,y:Alph*. x R y
5. 
x,y,z:Alph*. (x R y) 
((z @ x) R (z @ y))
6. g: (x,y:Alph*//(x R y))
7. l:Alph*. L(l) 
g(l)
8. Alph* = Alph*
9. x: Alph*
10. y: Alph*
(x L-induced Equiv y) (x Rg y)
By: Inst
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)))
[Alph;R;g;L;x;y]
Generated subgoal:| 1 | L  LangOver(Alph) |
About:
