| Some definitions of interest. |
|
exists_unique | Def !x:A. P(x) == x:A. x is the x:A. P(x) |
| | Thm* A:Type, P:(A Prop). ( !x:A. P(x)) Prop |
|
inhabited_uniquely | Def ! A ==  {x:A| y:A. x = y } |
|
is_the | Def x is the u:A. P(u) == P(x) & ( u:A. P(u)  u = x) |
| | Thm* A:Type, P:(A Prop), x:A. (x is the x:A. P(x)) Prop |