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