2. R: Alph*
Alph*Prop3. EquivRel x,y:Alph*. x R y
4.
x,y,z:Alph*. (x R y) 
((z @ x) R (z @ y))5. z1: Alph*
6. z2: Alph*
7. y: x,y:Alph*//(x R y)
z1 @ z2@
y = z1@z2@y Alph:Type, R:(Alph*Alph*Prop).
(EquivRel x,y:Alph*. x R y)
(x,y,z:Alph*. (x R y) ((z @ x) R (z @ y)))
(z1,z2:Alph*, y:x,y:Alph*//(x R y). z1 @ z2@y = z1@z2@y)| 1 | 1. Alph: Type 2. R: Alph* Alph*Prop3. EquivRel x,y:Alph*. x R y 4. x,y,z:Alph*. (x R y) ((z @ x) R (z @ y))5. z1: Alph* 6. z2: Alph* 7. y: x,y:Alph*//(x R y) z1 @ z2@y = z1@z2@y |
About:
 |  |  |  |  |  |  |  |