| 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 |
|
increasing | Def increasing(f;k) == i: (k-1). f(i)<f(i+1) |
| | Thm* k: , f:( k  ). increasing(f;k) Prop |