a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
  (with ds: ds action a:T precondition a(v) is P s v)  MsgA

By:	Auto THEN Unfold `ma-single-pre` 0 THEN Analyze THEN Reduce 0 THEN Try (Complete (Auto THEN Using [`B',(x. Type)] Auto))

1

1. a : Id 2. T : Type 3. ds : x:Id fp-> Type 4. P : State(ds)TProp   a : P  a@0:Id fp-> State(ds)ma-valtype(locl(a) : T; locl(a@0))Prop

5 steps

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