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