This coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators.

this package provides the plugin itself.