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

this package provides the coq support library.