(def-schematic-macete abstraction-for-induction
  "with(p:prop,kk:zz, forall(mm:zz,(kk<=mm implies p)) iff 
forall(mm:zz,(kk<=mm implies lambda(mm:zz,p)(mm))))"
  null
  (theory h-o-real-arithmetic))

(def-schematic-macete iteration-operator-eliminate-local-context-unsafe
  "with(op:[zz,zz,[zz,rr],rr], forall(x:rr,pp:prop,a,b:zz,
op(a,b,lambda(j:zz,if(pp,x,0)))=op(a,b,lambda(j:zz,x))))"
  null
  (theory h-o-real-arithmetic))