(2steps total) 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-sub weakening
  M1,M2:MsgA. M1 = M2  M1  M2
By: Auto THEN HypSubst -1 0 THEN All Thin

Generated subgoal:

1 1. M2 : MsgA
  M2  M2
1 step

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

(2steps total) PrintForm Definitions Lemmas mb event system 5 Sections EventSystems Doc