The $\lambda$$\Pi$-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$$\Pi$-calculus modulo theory by equational axioms, when this theory features the notions of proposition and proof, while maintaining the same expressiveness. To do so, we introduce in the target theory a heterogeneous equality, and we build a translation that replaces each use of the conversion rule by the insertion of a transport. At the end, the theory with rewrite rules is a conservative extension of the theory with axioms.

翻译：$λΠ$-演算模理论是简单类型 $λ$-演算的扩展，引入了依赖类型和用户定义的重写规则。我们证明，当理论具备命题与证明的概念时，可以用等式公理替换 $λΠ$-演算模理论中的重写规则，同时保持相同的表达能力。为此，我们在目标理论中引入异质等式，并构建一种翻译，将转换规则的每次使用替换为传输机制的插入。最终，包含重写规则的理论是包含公理理论的保守扩展。