Def interleaving(T;L1;L2;L)
Def == ||L|| = ||L1||+||L2||   & disjoint_sublists(T;L1;L2;L)

is mentioned by

Thm* L,L1,L2:T List. interleaving(T;L1;L2;L)  L1  L	[interleaving_sublist]
Thm* L1,L:T List. interleaving(T;L1;nil;L)  L = L1	[nil_interleaving2]
Thm* L1,L:T List. interleaving(T;nil;L1;L)  L = L1	[nil_interleaving]

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