Nuprl - mb_event_system_3 LEMMAs for member_DASH_es_DASH

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

Rank	Theorem	Name
4	Thm* es:ES, e,e',ev:E. (ev [e, e']) e ev & ev e'	[member-es-interval]
cites the following:
0	Thm* es:ES, e,e':E. es-ble{i:l}(es;e;e') e e'	[assert-es-ble]
0	Thm* x:T. (x nil) False	[nil_member]
1	Thm* l:T List, a,x:T. (x [a / l]) x = a (x l)	[cons_member]
3	Thm* the_es:ES, e',e:E. (e before(e')) (e <loc e')	[member-es-before]
2	Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2)	[member_append]
2	Thm* P:(T), L:T List, x:T. (x filter(P;L)) (x L) & P(x)	[member_filter]

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