Nuprl - mb_event_system_6 LEMMAs for assert_DASH_ma_DASH_join_DASH_list_DASH_is_DASH

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
6	Thm* L:MsgA List. ma-is-empty((L)) reduce(M,x. ma-is-empty(M) & x;True;L)	[assert-ma-join-list-is-empty]
cites the following:
5	Thm* L:MsgA List. ma-is-empty((L)) ~ reduce(M,x. ma-is-empty(M)x;true;L)	[ma-join-list-is-empty]

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html