| | Who Cites hall? |
|
| hall | Def all ==  p:'a   .   x:'a. (p(x)) |
| | | Thm* 'a:S. all  (('a hbool) hbool) |
|
| ball | Def x:T. P(x) ==  (x:T.  P(x)) |
| | | Thm* T:Type, P:(T). (x:T. P(x)) |
|
| bool | Def == Unit+Unit |
| | | Thm* Type |
| | | Thm* S |
|
| tlambda | Def (x:T. b(x))(x) == b(x) |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| prop_to_bool | Def P == InjCase(lem(P) ; true ; false) |
| | | Thm* P:Prop. (P) |
|
| ifthenelse | Def if b t else f fi == InjCase(b ; t; f) |
| | | Thm* b:, A:Type, p,q:A. if b p else q fi A |
|
| bfalse | Def false == inr( ) |
| | | Thm* false |
|
| btrue | Def true == inl() |
| | | Thm* true |
