IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-empty-frame-compatible-right A:MsgA. ma-frame-compatible(A; )
By:
Auto THEN Unfolds [`ma-empty`;`ma-frame-compatible`] 0 THEN Unfold_MsgA -1
THEN
Reduce 0
THEN
FpfSubtype
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html