Def interleaving_occurence(T;L1;L2;L;f1;f2)
Def == ||L|| = ||L1||+||L2||  
Def == & increasing(f1;||L1||) & (j:||L1||. L1[j] = L[(f1(j))]  T)
Def == & increasing(f2;||L2||) & (j:||L2||. L2[j] = L[(f2(j))]  T)
Def == & (j1:||L1||, j2:||L2||. f1(j1) = f2(j2)  )

is mentioned by

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

[interleaving_split]

Try larger context: MarkB generic IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html