add more documentation for `simpl rewrite`

As discussed at #553.
Note: I think we can nearly duplicate `erewrite` (modulo cases where the term doesn't typecheck until typeclasses are filled in, and the choice of typeclasses depends on subterm selection) simply by changing `rewrite` to `erewrite` and using `open_constr`.  And I think we can nearly duplicate `rewrite` (modulo the same concerns), if we really want to, by explicitly checking that the term has no evars after we've rewritten with it.  (However, this has different behavior if there are user-inserted evars, I think.)