(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))