Nuprl - mb_list_2 LEMMAs for sublist

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

Rank	Theorem	Name
4	Thm* L1,L2:T List, P:(T). L2 filter(P;L1) L2 L1 & (xL2.P(x))	[sublist_filter]
cites the following:
3	Thm* x:T, L:T List. [x / L] nil False	[cons_sublist_nil]
0	Thm* L:T List. nil L True	[nil_sublist]
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* P:(TProp), x:T, L:T List. (y[x / L].P(y)) P(x) & (yL.P(y))	[l_all_cons]

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