M1,M2:MsgA.
  M1  M2
  
  (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x).
  (M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w))

By:

RepeatFor 8 (Analyze 0 THENA Complete Auto) THEN Unfold_MsgA -8 THEN Unfold_MsgA -7 THEN SplitAndHyps THEN Unfold `fpf-val` 0 THEN Try (DoSubsume THEN Reduce 0) THEN AllHyps (h.Unfold `fpf-sub` h THEN InstHyp [<k,x>] h THENA Complete Auto) THEN ExRepD THEN ThinTrivial THEN RevHypSubst -2 -1 THEN Try (DoSubsume THEN Reduce 0) THEN RevHypSubst -1 0 THEN Try (Fold `member` 0) THEN DoSubsume THEN BackThru Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g  f  (f(x)?T r g(x)?Top)

None

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