a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
  T
  
  xdom(ds). A=ds(x)   A
  
  (s:State(ds). Dec(v:T. P(s,v)))
  
  Feasible((with ds: ds
  Faction a:T
  Fprecondition a(v) is
  FP s v))

By:

ProveItFeasible THEN DVar `ds' THEN Reduce 0 THEN All (i.Repeat (Unfolds [`fpf-all`;`fpf-ap`;`fpf-dom`] i) THEN Reduce i) THEN Try BackThruSomeHyp THEN Try (OrLeft THEN Complete Auto) THEN SplitOnConclITE THEN Analyze -2 THEN RW assert_pushdownC -3 THEN Analyze -3 THEN All (RWO "deq_property<") THEN Analyze

None

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