| Who Cites bexists? |
|
bexists | Def  x:T. P(x) ==  ( x:T. P(x)) |
| | Thm* T:Type, P:(T  ). ( x:T. P(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  |