PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-is-empty-sub
  A,B:MsgA. ma-is-empty(A)  A  B
By: RWO Thm* M:MsgA. ma-is-empty(M)  M =   MsgA 0 THEN HypSubst -1 0
THEN
BackThru Thm* M:MsgA.   M

Generated subgoals:

None

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

PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc