x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
  f:(State(ds)ma-valtype(da; k)ds(x)?Void).
  xdom(ds). A=ds(x)   A
  
  kdom(da). A=da(k)   A  Feasible(ma-single-effect(ds; da; k; x; f))

By:

((ProveItFeasible THEN DVar `da' THEN Reduce 0 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 ((DupHyp -1 ((THEN ((RWO Thm* eq:EqDecider(A), L:A List, x:A. deq-member(eq;x;L)  (x  L) -1) (THEN (OrLeft) THEN Try BackThruSomeHyp

None

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