The substitution lemma is a renowned theorem within the realm of lambda-calculus theory and concerns the interactional behaviour of the metasubstitution operation. In this work, we augment the lambda-calculus's grammar with an uninterpreted explicit substitution operator, which allows the use of our framework for different calculi with explicit substitutions. Our primary contribution lies in verifying that, despite these modifications, the substitution lemma continues to remain valid. This confirmation was achieved using the Coq proof assistant. Our formalization methodology employs a nominal approach, which provides a direct implementation of the alpha-equivalence concept. The strategy involved in variable renaming within the proofs presents a challenge, specially on ensuring an exploration of the implications of our extension to the grammar of the lambda-calculus.

翻译：代入引理是λ演算理论领域的一个著名定理，涉及元代入运算的交互行为。本研究通过引入未经解释的显式代入算子扩展了λ演算的语法，使得我们的框架可适用于不同带显式代入的演算系统。主要贡献在于验证了尽管经过这些修改，代入引理仍然成立。此项验证通过Coq证明辅助工具实现。形式化方法采用名义化方法，从而直接实现α等价概念。证明过程中的变量重命名策略存在一定挑战，尤其是在确保我们扩展对λ演算语法影响的具体探索方面。