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. increasing(f;||L2||)
17.
j:||L2||. L2[j] = L[(f(j))]
18. L1 : T List
19. ||L1|| = k
20. increasing(g;||L1||)
21.
j:||L1||. L1[j] = L[(g(j))]
||L|| = ||L2||+||L1|| 
& (j1:||L2||, j2:||L1||. f(j1) = g(j2))
