T:Type, L:T List, P:(||L||Prop).
  (x:||L||. Dec(P(x)))
  
  (L1,L2:T List, f1:(||L1||||L||), f2:(||L2||||L||).
  (interleaving_occurence(T;L1;L2;L;f1;f2)
  (& (i:||L1||. P(f1(i))) & (i:||L2||. P(f2(i)))
  (& (i:||L||. 
  (& ((P(i)  (j:||L1||. f1(j) = i)) & (P(i)  (j:||L2||. f2(j) = i))))

1

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))   L1,L2:T List, f1:(||L1||||L||), f2:(||L2||||L||).   interleaving_occurence(T;L1;L2;L;f1;f2)   & (i:||L1||. P(f1(i))) & (i:||L2||. P(f2(i)))   & (i:||L||.    & ((P(i)  (j:||L1||. f1(j) = i)) & (P(i)  (j:||L2||. f2(j) = i)))

21 steps

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