| Who Cites le int? |
|
le_int | Def i j ==  j< i |
| | Thm* i,j: . (i j)  |
|
lt_int | Def i< j == if i<j true ; false fi |
| | Thm* i,j: . (i< j)  |
|
bnot | Def  b == if b false else true fi |
| | Thm* b: .  b  |
|
bfalse | Def false == inr( ) |
| | Thm* false  |
|
btrue | Def true == inl( ) |
| | Thm* true  |
|
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 |