1. T : Type
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))]
22. j1:||L2||, j2:||L1||. f(j1) = g(j2)
  ||L|| = ||L2||+||L1||  

1

23. i : ||L||   (j:||L2||. i = f(j))  (j:||L1||. i = g(j))

1 step

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