对 $𝑡$ 结构归纳（ 归纳证明的写法 ）． 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 的三个前提．