对 $𝑡$ 结构归纳（ [约定] 归纳证明的写法 ），对 $𝑇$、${𝑇}^{\prime }$ 一般化。

• 常量、$\text{succ }{𝑡}_1$、$\text{pred }{𝑡}_1$、$\text{iszero }{𝑡}_1$：由 [引理] 反演 ，类型被项的形状直接定死（$\text{Bool}$ 或 $\text{Nat}$），所以 $𝑇={𝑇}^{\prime }$。
• $\text{if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3$：由 [引理] 反演 第 2 条，${𝑡}_2:𝑇$ 且 ${𝑡}_2:{𝑇}^{\prime }$。${𝑡}_2$ 是直接子项，由 归纳假设 $𝑇={𝑇}^{\prime }$。