The rewrite tactic (rw)
=======================