M1,M2:MsgA.
  M1  M2  (k:Knd, x:Id. M2.frame(k affects x)  M1.frame(k affects x))

By:

((Auto THEN Unfold_MsgA -6 THEN Unfold_MsgA -5 THEN ExRepD THEN ParallelOp -1 ((THEN ((Analyze 0) (THEN ((Analyze -2)) THEN AllHyps (h. (Unfold `fpf-sub` h THEN InstHyp [x] 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 [x] h THENA Complete Auto THEN Analyze -1)

None

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