Nuprl - graph_1_1 LEMMAs for l_before_append

Rank	Theorem	Name
5	Thm* A,B:T List, x,y:T. x before y A @ B x before y A x before y B (x A) & (y B)	[l_before_append_iff]
cites
4	Thm* C,A,B:T List. C A @ B (A',B':T List. C = (A' @ B') & A' A & B' B)	[sublist_append_iff]
0	Thm* x:T, L:T List. (x L) [x] L	[member_iff_sublist]
2	Thm* L1,L2,L3:T List. L1 L2 L2 L3 L1 L3	[sublist_transitivity]
1	Thm* x1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2	[cons_sublist_cons]