M1,M2:MsgA.
  M1  M2
  
  (a:Id, s:M2.state.
  (a declared in M1  unsolvable M2.pre(a,s)  unsolvable M1.pre(a,s))

By:

RepeatFor 6 (Analyze 0 THENA Complete Auto) THEN Unfold_MsgA -6 THEN Unfold_MsgA -5 THEN SplitAndHyps THEN Unfold `fpf-val` 0 THEN AllHyps (h.Unfold `fpf-sub` h THEN InstHyp [a] h THENA Complete Auto) THEN AllHyps (h.Unfold `fpf-sub` h THEN InstHyp [locl(a)] h THENA Complete Auto) THEN ExRepD THEN ThinTrivial THEN AssertBY (d2(locl(a))?Top = da(locl(a))?Top) (Unfold `fpf-cap` 0 THEN SplitOnConclITE THEN SplitOnConclITE) THEN HypSubst -5 0 THEN BackThruSomeHyp

None

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