IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-decla-sub M1,M2:MsgA. M1M2 (a:Id. a declared in M1a declared in M2)
By:
RepeatFor 4 (Analyze 0) THEN Unfold_MsgA -4 THEN Unfold_MsgA -3 THEN ExRepD
THEN
AllHyps (h.Unfold `fpf-sub` h THEN InstHyp [locl(a)] h THENA Complete Auto)
THEN
ExRepD
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
M1,M2:MsgA. M1 
M2 
(
h.Unfold `fpf-sub` h THEN InstHyp [locl(a)] h THENA Complete Auto)
