The generalized rewriting tactic

The grw/grewrite tactic is a generalization of the rewrite tactic that works with relations other than equality. The core implementation of grewrite is in the file Tactic.GRewrite.Core