IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-sub-join-right M1,M2:MsgA. M1 || M2M2M1M2
By:
Auto THEN Unfold `ma-compatible` -1 THEN Unfold_MsgA -3 THEN Unfold_MsgA -2
THEN
BackThru
Thm*B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f || ggfg THEN
All (Unfold `ma-valtype`)
THEN
DoSubsume
THEN
ProveFpfSub
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
M1,M2:MsgA. M1 || M2 
M2 
M1 
M2
Type), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g 
