[引理] 反演 的逐形状证明依赖 [定义] 类型与类型判断 的语法导向性：每种项形状只对应一条规则。如果将来加一条不看项形状的规则（例如子类型里常见的“若 $𝑡:𝑆$ 且 $𝑆$ 是 $𝑇$ 的子类型，则 $𝑡:𝑇$”），那么 $\text{succ }{𝑡}_1:𝑇$ 的最后一步就可能是这条新规则，“最后一步必然是 T-Succ”的推理就断了。到那时反演需要重新陈述、重新证明。