q*) ~ 
h:(q*
q*). (
x,y:q*. (x E y) 
h(x) = h(y)) & (x:q*. x E (h(x)))
q*q*Propq*. x E yx,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)))q:. (q*) ~
[q]| 1 | 5. (q*) ~ h:(q*q*). (x,y:q*. (x E y) h(x) = h(y)) & (x:q*. x E (h(x))) |
About:
 |  |  |  |  |
 |  |  |  |