(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 1
1. M2 : MsgA
  M2  M2
By: Unfold_MsgA -1
THEN
BackThru Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g  f  g

Generated subgoals:

None

About:
functionuniverseequalimpliesall
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