| Who Cites bimplies? |
|
bimplies | Def p  q ==  p  q |
| | Thm* p,q: . p  q  |
|
bnot | Def  b == if b false else true fi |
| | Thm* b: .  b  |
|
bor | Def p  q == if p true else q fi |
| | Thm* p,q: . (p  q)  |
|
btrue | Def true == inl( ) |
| | Thm* true  |
|
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 |