(
x,y:
q*. (x E y) 
Id(x) = Id(y) 
q*) & (x:q*. x E (Id(x)))
0 < qq*
q*Propq*. x E y) & (x,y:q*. Dec(x E y)) 
h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x)))| 1 | (x,y:q*. (x E y) Id(x) = Id(y) q*) & (x:q*. x E (Id(x))) |
About:
 |  |  |  |  |
 |  |  |  |  |