Coq Modulo Theories (CoqMT) is an extension of the Coq proof assistant embedding, in its computational mechanism, validity entailment for user-defined first-order equational theories.
Download
Last version of CoqMT is 8.3pl3.