Def == (
x:'a. p(x))
(
x,y:'a. (p(x)p(y))
(x = y))'a:Type, p:('a
). b_exists_unique('a;x.p(x)) 
b == if b
True else False fib:. b Prop
Q == (P Q) & (P Q)A,B:Prop. (A B) Prop| Some definitions of interest. | |
| b_exists_unique | Def == ( x:'a. p(x))(x,y:'a. (p(x)p(y))(x = y)) |
| 'a:Type, p:('a). b_exists_unique('a;x.p(x)) | |
| assert | b == if b True else False fi |
| b:. b Prop | |
| iff | Q == (P Q) & (P Q) |
| A,B:Prop. (A B) Prop |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |