反演 中直接确定最后一条规则的证明， 依赖 类型与类型判断 的语法导向性质： 每种项形状只对应一条候选规则． 如果将来加一条不看项形状的规则 （例如子类型里常见的“若 $𝑡:𝑆$ 且 $𝑆<:𝑇$，则 $𝑡:𝑇$”）， 那么 $\text{succ }{𝑡}_1:𝑇$ 的最后一步就可能是这条新规则， “最后一步必然是 T-Succ”的推理就断了． 非语法导向的系统仍可证明反演引理，但届时需重新陈述结论，没法直接沿用这份逐形状的证明．