2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6.
i,j:
. i<||L|| 
j<||L|| 
i = j L[i] = L[j]
7. f1 :
||L1 @ [x]||
||L||
8. increasing(f1;||L1 @ [x]||)
9.
j:||L1 @ [x]||. (L1 @ [x])[j] = L[(f1(j))]
10. f :
(||L2||+1)||L||
11. increasing(f;||L2||+1)
12.
j:(||L2||+1). [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||nil||
0
15. j :
||L1 @ [x / L2]||
16. ||L1 @ [x]|| = ||L1||+1
17. ||L1||<j
[x / L2][(j-||L1||)] = L[(f(j-||L1||))]
