mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
3Thm* L1,L2:T List. L1  L2  L2  L1  L1 = L2[sublist_antisymmetry]
cites the following:
2Thm* L1,L2:T List. L1  L2  ||L1|| = ||L2||    L1 = L2[proper_sublist_length]
2Thm* L1,L2:T List. L1  L2  ||L1||||L2||[length_sublist]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb list 1 Sections MarkB generic Doc