IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-sub-join-left M1,M2:MsgA. M1M1M2
By:
All_MsgA THEN Analyze 0 THEN Unfold_MsgA -1
THEN
BackThru
Thm*B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a).
Thm* ffg 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 
M1 
M2
Type), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a).
