This package provides tools to prove equational theorems: from a mathematical specification in many-sorted first-order logic with equality and an hypothesis/conjecture, it will look for a proof.