Various implementations of rewriting with setoids.

- Man work is in AutoSetoidRewrite.
bug fix to rewriting.

- Demo rewriting for quantifier pulling
  - Need to figure out how to do alternation.