M1,M2,M3:MsgA. M1  M2  M2  M3  M1  M3

By:	Auto THEN Unfold_MsgA -5 THEN Unfold_MsgA -4 THEN Unfold_MsgA -3 THEN ExRepD THEN BetterSplitAndConcl THEN SimpleTransitivity THEN Try (DoSubsume THEN ProveFpfSub) THEN AllHyps (h. (MoveToConcl h THEN BackThru Thm: fpf-sub functionality THEN Try DoSubsume (THEN (ProveFpfSub)

None

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