在 保型 的证明中， E-If 是 一步规约 的条件规约规则， 类型关系采用 类型与类型判断 ． 处理这个情形时， 归纳假设 用在 ${𝑡}_1$ 上，而 ${𝑡}_1$ 的类型是 $\text{Bool}$，不一定是 $𝑡$ 的类型 $𝑇$． 如果待证性质写成“对这个固定的 $𝑇$，${𝑡}^{\prime }:𝑇$”， 归纳假设 就只能谈论这个 $𝑇$，在这里用不上． 所以待证性质必须写成“对任意 $𝑇$，若 $𝑡:𝑇$ 则 ${𝑡}^{\prime }:𝑇$”． 这个细节在自然语言的证明里很容易略过； 确定性 的证明里对 ${𝑡}^{″}$ 也做了同样的处理．