use `open_constr` in `simpl rewrite`
`simpl rewrite` with `Arguments` solves the rewrite problems in Factorization
add comments about Set Debug Tactic Unification
Merge pull request #583 from mikeshulman/rewrites

'simpl rewrite' can solve the problems in Factorization