Abstract The $$\lambda \varPi $$ λ Π -calculus modulo theory is an extension of simply typed $$\lambda $$ λ -calculus with dependent types and user-defined rewrite rules. We show that it is possible to replace the rewrite rules of a theory of the $$\lambda \varPi $$ λ Π -calculus modulo theory by eq...