2. E: T
TProp3. EquivRel x,y:T. x E y
4. x: T
5. y: T
6. x = y
x = y 
u,v:T//(u E v) 
T:Type, E:(TTProp). (EquivRel x,y:T. x E y) 
(x,y:T. x = y x = y u,v:T//(u E v))| 1 | 1. T: Type 2. E: T TProp3. EquivRel x,y:T. x E y 4. x: T 5. y: T 6. x = y x = y u,v:T//(u E v) |
About:
 |  |  |  |  |  |  |