2. L: Alph*
Prop3. R: Alph*
Alph*Prop4. 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)
x,y:Alph*//(x L-induced Equiv y) = x,y:Alph*//(x Rg y) Alph:Type, 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))| 1 | 1. Alph: Type 2. L: Alph* Prop3. R: Alph* Alph*Prop4. 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) x,y:Alph*//(x L-induced Equiv y) = x,y:Alph*//(x Rg y) |
About:
 |  |  |  |  |  |
 |  |  |  |  |