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. ||L|| = ||L1||+||L2||
12. increasing(f1;||L1||)
13.
j:||L1||. L1[j] = L[(f1(j))]
14. increasing(f2;||L2||)
15.
j:||L2||. L2[j] = L[(f2(j))]
16.
j1:||L1||, j2:||L2||. 
f1(j1) = f2(j2)
17.
i:||L1||. P(f1(i))
18.
i:||L2||. P(f2(i))
19.
i:||L||.
19. (P(i)
(
j:||L1||. f1(j) = i)) & (P(i) (j:||L2||. f2(j) = i))
20. 0<||L1||
21. j :
||L||
22. f1(||L1||-1)<j
23. P(j)
24.
P(j) (j@0:||L2||. f2(j@0) = j)
25. j@0 :
||L1||
26. f1(j@0) = j
27.
x,y:||L1||. x<y f1(x)<f1(y)
28.
j@0<||L1||-1
False
