L1,L:T List. interleaving(T;L1;nil;L) 
L = L1L1,L2,L:T List. disjoint_sublists(T;L1;L2;L) 
L1 
L & L2 LL1,L2:T List. L1 L2 ||L1|| = ||L2|| 
L1 = L2| Rank | Theorem | Name |
| 3 | L1,L:T List. interleaving(T;L1;nil;L) L = L1 | [nil_interleaving2] |
| cites the following: | ||
| 0 | L1,L2,L:T List. disjoint_sublists(T;L1;L2;L) L1 L & L2 L | [disjoint_sublists_sublist] |
| 2 | L1,L2:T List. L1 L2 ||L1|| = ||L2|| L1 = L2 | [proper_sublist_length] |