1. T : Type
2. L : T List
3. P : ||L||Prop
4. x:||L||. Dec(P(x))
5. i : ||L||
6. P(i)
7. L1 : T List
8. L2 : T List
9. f1 : ||L1||||L||
10. f2 : ||L2||||L||
11. interleaving_occurence(T;L1;L2;L;f1;f2)
12. i:||L1||. P(f1(i))
13. i:||L2||. P(f2(i))
14. i:||L||. 
14. (P(i)  (j:||L1||. f1(j) = i)) & (P(i)  (j:||L2||. f2(j) = i))
15. 0<||L1||
16. j : ||L||
17. f1(||L1||-1)<j
18. P(j)
19. P(j)  (j@0:||L2||. f2(j@0) = j)
20. j@0 : ||L1||
21. f1(j@0) = j
  False

By:	AllHyps (i. (Unfold `interleaving_occurence` i THEN ExRepD (THEN (FwdThru Thm* k:, f:(k). increasing(f;k)  (x,y:k. x<y  f(x)<f(y)) ([i+1])

1

11. ||L|| = ||L1||+||L2||   12. increasing(f1;||L1||) 13. j:||L1||. L1[j] = L[(f1(j))] 14. increasing(f2;||L2||) 15. j:||L2||. L2[j] = L[(f2(j))] 16. j1:||L1||, j2:||L2||. f1(j1) = f2(j2) 17. i:||L1||. P(f1(i)) 18. i:||L2||. P(f2(i)) 19. i:||L||.  19. (P(i)  (j:||L1||. f1(j) = i)) & (P(i)  (j:||L2||. f2(j) = i)) 20. 0<||L1|| 21. j : ||L|| 22. f1(||L1||-1)<j 23. P(j) 24. P(j)  (j@0:||L2||. f2(j@0) = j) 25. j@0 : ||L1|| 26. f1(j@0) = j 27. x,y:||L1||. x<y  f1(x)<f1(y)   False

3 steps

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