Nuprl - mb_event_system_1 LEMMAs for before_DASH

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

Rank	Theorem	Name
5	Thm* f:(TT'), L:T List, x',y':T'. Thm* x' before y' map(f;L) (x,y:T. x before y L & f(x) = x' & f(y) = y')	[before-map]
cites the following:
4	Thm* x,y:T. x before y nil False	[nil_before]
2	Thm* l:T List, a,x,y:T. Thm* x before y [a / l] x = a & (y l) x before y l	[cons_before]
2	Thm* a:T List, x:T', f:(TT'). (x map(f;a)) (y:T. (y a) & x = f(y))	[member_map]

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