| | Some definitions of interest. |
|
| hselect | Def select ==  p:'a   . @ x:'a. (p(x)) |
| | | Thm*  'a:S. select  (('a hbool) 'a) |
|
| bchoose | Def @x:'a. p(x) == @x:'a.  p(x) |
| | | Thm* 'a:S, p:('a). (@x:'a. p(x)) 'a |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| hand | Def and == p:. q:. p  q |
| | | Thm* and (hbool hbool hbool) |
|
| band | Def pq == if p q else false fi |
| | | Thm* p,q:. (pq) |
|
| hnot | Def not == p:.  p |
| | | Thm* not (hbool hbool) |
|
| bnot | Def b == if b false else true fi |
| | | Thm* b:. b |
|
| hsuc_rep | Def suc_rep == x: . (@f:. (one_one(;;f) & onto(;;f)))(x) |
| | | Thm* suc_rep (hind hind) |
|
| choose | Def @x:T. P(x) == InjCase(lem({x:T| P(x) }); x. x, arb(T)) |
| | | Thm* T:S, P:(TType). (@x:T. P(x)) T |
|
| hequal | Def equal == x:'a. y:'a. x = y |
| | | Thm* 'a:S. equal ('a 'a hbool) |
|
| hfun | Def 'a 'b == 'a'b |
| | | Thm* 'a,'b:S. ('a 'b) S |
|
| hind | Def hind == |
| | | Thm* hind S |
|
| hone_one | Def one_one == f:'a'b.  one_one('a;'b;f) |
| | | Thm* 'a,'b:S. one_one (('a 'b) hbool) |
|
| honto | Def onto == f:'a'b. onto('a;'b;f) |
| | | Thm* 'a,'b:S. onto (('a 'b) hbool) |
|
| label | Def t ...$L == t |
|
| nat | Def == {i: | 0 i } |
| | | Thm* Type |
| | | Thm* S |
|
| not | Def A == A   False |
| | | Thm* A:Prop. (A) Prop |
|
| one_one | Def one_one('a;'b;f) == x,y:'a. f(x) = f(y) 'b x = y |
| | | Thm* 'a,'b:Type, f:('a'b). one_one('a;'b;f) Prop |
|
| onto | Def onto('a;'b;f) == y:'b.  x:'a. y = f(x) |
| | | Thm* 'a,'b:Type, f:('a'b). onto('a;'b;f) Prop |
|
| prop_to_bool | Def P == InjCase(lem(P) ; true; false) |
| | | Thm* P:Prop. (P) |
|
| tlambda | Def (x:T. b(x))(x) == b(x) |
