more sf-poly higher order examples; need to explicit curry
smarter lazy encoding of terms to avoid redundant SMT coding