(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 interleaving 1
1. T : Type
2. L1 : T List
3. L : T List
4. ||L|| = 0+||L1||
5. disjoint_sublists(T;nil;L1;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. nil  L
7. L1  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