2. L : T List
3. P :
||L||
Prop
4.
x:||L||. Dec(P(x))
5. i :
||L||
6. P(i)
7. L1 : T List
8. L2 : T List
9. f1 :
||L1||||L||
10. f2 :
||L2||||L||
11. interleaving_occurence(T;L1;L2;L;f1;f2)
12.
i:||L1||. P(f1(i))
13.
i:||L2||. 
P(f2(i))
14.
i:||L||.
14. (P(i)
(
j:||L1||. f1(j) = i)) & (P(i) (j:||L2||. f2(j) = i))
0<||L1||
