对 $𝑡:𝑇$ 作规则归纳 （类型推导版本的 规则归纳法 ）， 按最后一步的规则分情形．

若最后一步是 T-True、T-False 或 T-Zero，则 $𝑡$ 本身就是值． 若最后一步是 T-If，则 $𝑡=\text{ if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3$，前提里有 ${𝑡}_1:\text{ Bool}$；对 ${𝑡}_1$ 用 归纳假设 ，若 ${𝑡}_1$ 能规约，由 E-If 知 $𝑡$ 也能规约；若 ${𝑡}_1$ 是值，由 典范形式 第 1 条知它是 $\text{true}$ 或 $\text{false}$，可分别用 E-IfTrue、E-IfFalse． 若最后一步是 T-Succ，前提为 ${𝑡}_1:\text{ Nat}$；若 ${𝑡}_1$ 能规约，用 E-Succ；若 ${𝑡}_1$ 是值，由 典范形式 第 2 条知它是数值 nv，于是 t = succ nv 本身也是数值，自然也是值． 若最后一步是 T-Pred，前提为 ${𝑡}_1:\text{ Nat}$；若 ${𝑡}_1$ 能规约，用 E-Pred；若 ${𝑡}_1$ 是值，则它是数值，等于 $0$ 时用 E-PredZero，形如 succ nv' 时用 E-PredSucc． T-IsZero 的情形与 T-Pred 相同，分别用 E-IsZero、E-IsZeroZero、E-IsZeroSucc．