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
3	Thm* the_es:ES, e',e:E. (e before(e')) (e <loc e')	[member-es-before]
cites the following:
0	Thm* the_es:ES, j,e:E. first(j) (e <loc j)	[es-first-implies]
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]
2	Thm* x:T, l1,l2:T List. (x l1 @ l2) (x l1) (x l2)	[member_append]
1	Thm* the_es:ES, e,e':E. Thm* (e <loc e') first(e') & e = pred(e') E (e <loc pred(e'))	[es-locl-iff]
0	Thm* the_es:ES, j:E. first(j) (pred(j) <loc j)	[es-pred-locl]

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