| Who Cites hgt? |
|
hgt | Def gt == m: . n: . n< m |
| | Thm* gt (hnum  hnum  hbool) |
|
lt_int | Def i< j == if i<j true ; false fi |
| | Thm* i,j: . (i< j)  |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
| | Thm* S |
|
tlambda | Def ( x:T. b(x))(x) == b(x) |
|
bfalse | Def false == inr( ) |
| | Thm* false  |
|
btrue | Def true == inl( ) |
| | Thm* true  |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |