对 $𝑡$ 结构归纳（ [约定] 归纳证明的写法 ）。 type_of type_of 本身就是按项的形状分支的，所以每个情形对应一个分支。

• 常量： True True 、 False False 分支返回 Bool Bool ， Zero Zero 分支返回 Nat Nat ，分别是 T-True、T-False、T-Zero 的结论。
• $\text{succ }{𝑡}_1$：返回 Some(Nat) Some(Nat) 只有一种可能， type_of(t1) = Some(Nat) type_of(t1) = Some(Nat) 。由 归纳假设 ${𝑡}_1:\text{ Nat}$，用 T-Succ 得 $\text{succ }{𝑡}_1:\text{ Nat}$。$\text{pred}$、$\text{iszero}$ 同理，分别用 T-Pred、T-IsZero。
• $\text{if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3$：返回 Some(ta) Some(ta) 说明 type_of(c) = Some(Bool) type_of(c) = Some(Bool) 、 type_of(a) = Some(ta) type_of(a) = Some(ta) 、 type_of(b) = Some(ta) type_of(b) = Some(ta) 。三次使用 归纳假设 分别给出 ${𝑡}_1:\text{ Bool}$、${𝑡}_2:𝑇$、${𝑡}_3:𝑇$（$𝑇$ 即 ta ta ），正是 T-If 的三个前提。