Nuprl - Proof: ma-empty-compatible-left

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-empty-compatible-left

A:MsgA. || A

By:	Auto THEN Unfolds [`ma-empty`;`ma-compatible`] 0 THEN Unfold `ma-compatible-decls` 0 THEN Unfold_MsgA -1 THEN SplitAndConcl THEN Try (BackThru Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top. \|\| f)

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html