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
  f:(||L1 @ [x / L2]||||L||). 
  increasing(f;||L1 @ [x / L2]||)
  & (j:||L1 @ [x / L2]||. (L1 @ [x / L2])[j] = L[(f(j))])

By:	AssertBY (||nil||0) (Reduce 0) THEN InstConcl [i.if i||L1|| f1(i) else f(i-||L1||) fi]

1	14. ||nil||0   (i.if i||L1|| f1(i) else f(i-||L1||) fi)  ||L1 @ [x / L2]||||L||	1 step
2	14. ||nil||0   increasing(i.if i||L1|| f1(i) else f(i-||L1||) fi;||L1 @ [x / L2]||)   & (j:||L1 @ [x / L2]||.    & ((L1 @ [x / L2])[j] = L[((i.if i||L1|| f1(i) else f(i-||L1||) fi)(j))])	34 steps
3	14. ||nil||0 15. f2 : ||L1 @ [x / L2]||||L||   (increasing(f2;||L1 @ [x / L2]||)   (& (j:||L1 @ [x / L2]||. (L1 @ [x / L2])[j] = L[(f2(j))]))    Prop	Auto

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