L:T List, P:(
||L||
Prop).
Thm* (
x:||L||. Dec(P(x)))
Thm*
Thm* (
i:||L||. P(i)) (i:||L||. P(i) & (j:||L||. i<j 
P(j)))L:T List, P:(||L||Prop).
Thm* (
x:||L||. Dec(P(x)))
Thm*
Thm* (
L1,L2:T List, f1:(||L1||||L||), f2:(||L2||||L||).
Thm* (interleaving_occurence(T;L1;L2;L;f1;f2)
Thm* (& (
i:||L1||. P(f1(i))) & (i:||L2||. P(f2(i)))
Thm* (& (
i:||L||.
Thm* (& ((P(i)
(j:||L1||. f1(j) = i))
Thm* (& (& (
P(i) (j:||L2||. f2(j) = i))))k:, f:(k
). increasing(f;k) (x,y:k. x<y f(x)<f(y))