Def disjoint_sublists(T;L1;L2;L)
Def == f1:(||L1||||L||), f2:(||L2||||L||).
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* L1,L2,L:T List. disjoint_sublists(T;L1;L2;L)  L1  L & L2  L	[disjoint_sublists_sublist]
Def interleaving(T;L1;L2;L) Def == ||L|| = ||L1||+||L2||   & disjoint_sublists(T;L1;L2;L)	[interleaving]

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