| Some definitions of interest. |
|
iff | Def P  Q == (P  Q) & (P  Q) |
| | Thm* A,B:Prop. (A  B) Prop |
|
sublist | Def L1 L2
Def == f:( ||L1||  ||L2||).
Def == increasing(f;||L1||) & ( j: ||L1||. L1[j] = L2[(f(j))] T) |
| | Thm* T:Type, L1,L2:T List. L1 L2 Prop |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | Thm* A:Type, l:A List. ||l||  |
| | Thm* ||nil||  |