a':T. Q(a') 
a' = a)T:Type, a:T, Q:(T
Prop). (a = !x:T. Q(x)) 
Propy:T. P(y) y = x) }T:Type, P:(TProp). {!x:T | P(x)} Type| Some definitions of interest. | |
| uni_sat | a':T. Q(a') a' = a) |
| T:Type, a:T, Q:(TProp). (a = !x:T. Q(x)) Prop | |
| unique_set | y:T. P(y) y = x) } |
| T:Type, P:(TProp). {!x:T | P(x)} Type |
About:
 |  |  |  |  |
 |  |  |  |  |