== {i:| i 
0 } 
Type
== {i:| 0
i } TypeB == 
B < A
i,j:. (ij) Prop| Some definitions of interest. | |
| int_nzero | Def == {i:| i 0 } |
| Thm* Type | |
| nat | Def == {i:| 0i } |
| Thm* Type | |
| le | Def AB == B < A |
| Thm* i,j:. (ij) Prop |
About:
 |  |  |  |  |  |  |  |  |