M1,M2:MsgA.
  M1  M2
  
  (k:Knd, l:IdLnk, tg:Id.
  (M2.sframe(k sends <l,tg>)  M1.sframe(k sends <l,tg>))

By:

((Auto THEN Unfold_MsgA -7 THEN Unfold_MsgA -6 THEN ExRepD THEN ParallelOp -1 ((THEN ((Analyze 0) (THEN ((Analyze -2)) THEN AllHyps (h. (Unfold `fpf-sub` h THEN InstHyp [<l,tg>] h THENA Complete Auto THEN Analyze -1 (THEN (Complete Auto) THEN Try (NthHypEq -1 THEN Analyze THEN Analyze) THEN AllHyps (h. (Unfold `fpf-sub` h THEN InstHyp [<l,tg>] h THENA Complete Auto THEN Analyze -1)

None

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