(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
1. T : Type
2. L1 : T List
3. L : T List
4. ||L|| = 0+||L1||
5. disjoint_sublists(T;nil;L1;L)
6. nil  L
7. L1  L
  L = L1
By: Symmetry
THEN
BackThru Thm* L1,L2:T List. L1  L2  ||L1|| = ||L2||    L1 = L2

Generated subgoals:

None

About:
listnilintnatural_numberadduniverseequalimpliesall
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