(4steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nil interleaving2 1
1. T : Type
2. L1 : T List
3. L : T List
4. ||L|| = ||L1||+0
5. disjoint_sublists(T;L1;nil;L)
  L = L1
By: FwdThru Thm* L1,L2,L:T List. disjoint_sublists(T;L1;L2;L)  L1  L & L2  L
[-1]

Generated subgoal:

1 6. L1  L
7. nil  L
  L = L1
1 step

About:
listnilnatural_numberadduniverseequalimpliesandall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(4steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc