1. T : Type
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. i : (||L1 @ [x / L2]||-1)
16. i||L1||
17. ||L1||<i+1
18. f1(i)f1(||L1||)
19. ||L1||<||L1 @ [x]||
20. f1(||L1||) = f(0)
21. (L1 @ [x])[||L1||] = L[(f1(||L1||))]
22. j:. ||L1||<||L||  j<||L||  ||L1|| = j  L[||L1||] = L[j]
  L[(f1(||L1||))] = x

By:	RWO Thm* as,bs:T List, i:{||as||..(||as||+||bs||)}. (as @ bs)[i] = bs[(i-||as||)] -2

1

21. [x][(||L1||-||L1||)] = L[(f1(||L1||))] 22. j:. ||L1||<||L||  j<||L||  ||L1|| = j    L[||L1||] = L[j]   L[(f1(||L1||))] = x

1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html