a:Id, T,A:Type, x:Id, P:(ATProp).
  T
  
  A
  
  (a:A. Dec(v:T. P(a,v)))  Feasible(ma-single-pre1(x;A;a;T;x,v.P(x,v)))

By:

Auto THEN AssertBY (x : A  x:Id fp-> Type) Auto THEN Unfold `ma-single-pre1` 0 THEN BackThru Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* T Thm*  Thm* xdom(ds). A=ds(x)   A Thm*  Thm* (s:State(ds). Dec(v:T. P(s,v))) Thm*  Thm* Feasible((with ds: ds Thm* Faction a:T Thm* Fprecondition a(v) is Thm* FP s v)) THEN Try (Complete (Auto THEN Fold `ma-state` 0))

1

1. Id 2. T : Type 3. A : Type 4. x : Id 5. P : ATProp 6. T 7. A 8. a:A. Dec(v:T. P(a,v)) 9. x : A  x:Id fp-> Type   xdom(x : A). A=x : A(x)   A

1 step

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