E:(q*
q*Prop).
(EquivRel x,y:q*. 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))))q:
, E:(q*q*Prop).
(EquivRel x,y:q*. 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))))
[q]None
About:
| | | | | |
 |  |  |  |  |