Nuprl - mb_event_system_5 LEMMAs for ma_DASH_is_DASH_empty_DASH_sub

mb event system 5 Sections EventSystems Doc

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

Rank	Theorem	Name
3	Thm* A,B:MsgA. ma-is-empty(A) A B	[ma-is-empty-sub]
cites the following:
1	Thm* M:MsgA. M	[ma-empty-sub]
2	Thm* M:MsgA. ma-is-empty(M) M = MsgA	[assert-ma-is-empty]

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

mb event system 5 Sections EventSystems Doc