github.com/coq/opam-coq-archive
This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators
opam install coq-aac-tactics.8.11.0