Add many variants of the [simpl rewrite] tactic

It's unfortunate that Coq doesn't give us a notation of saying "this
takes anything that rewrite can take".  But these are useful for
making tactic scripts conceptually clearer.