2. m:
n3. E:
n
nProp4. EquivRel x,y:
n. x E y
Refl(m;x,y.x E y) & Sym x,y:m. x E y & Trans x,y:m. x E y 
n:{1...}, m:n, E:(nnProp). (EquivRel x,y:n. x E y) 
(EquivRel x,y:m. x E y)| 1 | 1. n: {1...} 2. m: n3. E: nnProp4. EquivRel x,y: n. x E y Refl(m;x,y.x E y) & Sym x,y:m. x E y & Trans x,y:m. x E y |
About:
 |  |  |  |  |  |