Nuprl - graph_1_1 LEMMAs for l_before

Rank	Theorem	Name
6	Thm* L:T List, x,y:T. x before y L (A,B:T List. L = (A @ B) & (x A) & (y B))	[l_before_decomp]
cites
3	Thm* x:T, L:T List. [x / L] nil False	[cons_sublist_nil]
1	Thm* x1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2	[cons_sublist_cons]
0	Thm* a,x:T. (x [a]) x = a	[member_singleton]
0	Thm* x:T, L:T List. (x L) [x] L	[member_iff_sublist]
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]