2. L : T List
3. P :
||L||
Prop
4.
x:||L||. Dec(P(x))
5. n :
6. k :
7. f :
n||L||
8. g :
k||L||
9. increasing(f;n)
10. increasing(g;k)
11.
i:n. P(f(i))
12.
j:k. 
P(g(j))
13.
i:||L||. (
j:n. i = f(j)) 
(j:k. i = g(j))
14. L2 : T List
15. ||L2|| = n
16. sublist_occurence(T;L2;L;f)
17. L1 : T List
18. ||L1|| = k
19. sublist_occurence(T;L1;L;g)
20. ||L|| = ||L2||+||L1||
21. increasing(f;||L2||)
22.
j:||L2||. L2[j] = L[(f(j))]
23. increasing(g;||L1||)
24.
j:||L1||. L1[j] = L[(g(j))]
25.
j1:||L2||, j2:||L1||. f(j1) = g(j2)
26. i :
||L||
27.
P(i)
28. j :
n
29. i = f(j)
30. Dec(P(i))
31.
j2:||L1||. f(j) = g(j2)
32. L2[j] = L[(f(j))]
33. (
j@0:n. j = f(j@0)) (j@0:k. j = g(j@0))
34. P(f(j))
35. Dec(P(j))
j:||L1||. g(j) = i
