| Who Cites hand? |
|
hand | Def and == p: . q: . p q |
| | Thm* and (hbool  hbool  hbool) |
|
band | Def p q == if p q else false fi |
| | Thm* p,q: . (p q)  |
|
bool | Def == Unit+Unit |
| | Thm* Type |
| | Thm* S |
|
tlambda | Def ( x:T. b(x))(x) == b(x) |
|
bfalse | Def false == inr( ) |
| | Thm* false  |
|
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 |