Def L1  L2
Def == f:(||L1||||L2||). 
Def == increasing(f;||L1||) & (j:||L1||. L1[j] = L2[(f(j))]  T)

is mentioned by

Thm* L,L1,L2:T List. interleaving(T;L1;L2;L)  L1  L	[interleaving_sublist]
Thm* L1,L2,L:T List. disjoint_sublists(T;L1;L2;L)  L1  L & L2  L	[disjoint_sublists_sublist]
Thm* L1,L2:T List, P:(T). L2  filter(P;L1)  L2  L1 & (xL2.P(x))	[sublist_filter]

In prior sections: mb list 1

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