| Some definitions of interest. |
|
boolsize | Def size( a)(p) == Msize( x.if p(x) 1 else 0 fi) |
| | Thm* a: . size( a) ( a  )   |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
msize | Def Msize(f) == i: k. f(i) |
| | Thm* k: . Msize ( k  )   |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |