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. sublist_occurence(T;L2;L;f)
17. L1 : T List
18. ||L1|| = k
19. sublist_occurence(T;L1;L;g)
20. interleaving_occurence(T;L2;L1;L;f;g)
  interleaving_occurence(T;L2;L1;L;f;g)
  & (i:||L2||. P(f(i))) & (i:||L1||. P(g(i)))
  & (i:||L||. 
  & ((P(i)  (j:||L2||. f(j) = i)) & (P(i)  (j:||L1||. g(j) = i)))

1	21. i : ||L|| 22. P(i)   j:||L2||. f(j) = i	5 steps
2	21. i : ||L|| 22. P(i)   j:||L1||. g(j) = i	5 steps

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