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
q == if p q else false fip,q:. (pq) y == (x = y T)T:Type, x,y:T. (x = y) 
q == 
p 
qp,q:. pq | 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 | |
| band | q == if p q else false fi |
| p,q:. (pq) | |
| bequal | y == (x = y T) |
| T:Type, x,y:T. (x = y) | |
| bimplies | q == p q |
| p,q:. pq |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |
 |