more cleanup to SetoidRewrite

- adding a lemma about typeof_expr and exprD ensuring
  the same type
- slight generalization of setoid_rewrite with a wrapper
  function to build a simpler interface.