Nuprl - mb_list_1 LEMMAs for l_before

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
3	Thm* l:T List, x,y,z:T. Thm* no_repeats(T;l) x before y l y before z l x before z l	[l_before_transitivity]
cites the following:
2	Thm* L1,L2,L3:T List. L1 L2 L2 L3 L1 L3	[sublist_transitivity]
1	Thm* x1,x2:T, L1,L2:T List. Thm* [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2	[cons_sublist_cons]
2	Thm* L1,L2,L:T List, x:T. Thm* no_repeats(T;L) L1 @ [x] L [x / L2] L L1 @ [x / L2] L	[append_overlapping_sublists]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html