| Some definitions of interest. |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
le | Def A B == B < A |
| | Thm* i,j: . (i j) Prop |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |
|
upto | Def upto(i;j) == if i < j [i / upto(i+1;j)] else nil fi (recursive) |
| | Thm* i,j: . upto(i;j) {i..j } List |