x:T. P(x) == 
(x:T. 
P(x))T:Type, P:(T
). (x:T. P(x)) 
b == if b
True else False fib:. b Prop y == (x = y T)T:Type, x,y:T. (x = y) 
q == 
p 
qp,q:. pq q == if p true else q fip,q:. (p q) | Some definitions of interest. | |
| ball | x:T. P(x) == (x:T. P(x)) |
| T:Type, P:(T). (x:T. P(x)) | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| bequal | y == (x = y T) |
| T:Type, x,y:T. (x = y) | |
| bimplies | q == p q |
| p,q:. pq | |
| bor | q == if p true else q fi |
| p,q:. (p q) |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |