mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
3Thm* L:T List, a,b:Ta before b  L  (b  L)[l_before_member]
cites the following:
0Thm* x:TL:T List. (x  L [x L[member_iff_sublist]
2Thm* L1,L2,L3:T List. L1  L2  L2  L3  L1  L3[sublist_transitivity]
2Thm* L1,L2:T List. null(L2 L1  tl(L2 L1  L2[sublist_tl]
1Thm* L1,L2:T List. L1 = L2  L1  L2[sublist_weakening]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb list 1 Sections MarkB generic Doc