x:'a. p(x) == @x:'a. 
p(x)
'a:S, p:('a
). (@x:'a. p(x)) 
'a y == 
(x = y T)T:Type, x,y:T. (x = y) 
== {i:
| 0
i } Type S
A == A 
FalseA:Prop. (A) Prop| Some definitions of interest. | |
| bchoose | x:'a. p(x) == @x:'a. p(x) |
| 'a:S, p:('a). (@x:'a. p(x)) 'a | |
| bequal | y == (x = y T) |
| T:Type, x,y:T. (x = y) | |
| nat | == {i:| 0i } |
| Type | |
| S | |
| not | A == A False |
| A:Prop. (A) Prop |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |