此命题描述了如何将替换 作用在另一个替换 上, 即逐项替换.

对 使用 -rule, 我们得到

观察 的语境和类型 , 注意到这相当于在一个更深的语境中添加一个新的, 类型为 的项, 该项从哪来? 自然是更深语境中的 , 所以我们这样考虑, 首先我们有 weakening,

通过复合 weakening, 我们可以 weaken 一个替换,

在 下, 我们通过添加 到这个替换的末尾, 来获得最终的代换,