对 $𝑡⟶{𝑡}^{\prime }$ 作规则归纳（ 规则归纳法 ），对 $𝑇$ 一般化． 每个情形先对 $𝑡:𝑇$ 使用 反演 ．

对 E-IfTrue，$𝑡=\text{ if }\text{ true }\text{ then }{𝑡}_2\text{ else }{𝑡}_3$，${𝑡}^{\prime }={𝑡}_2$，反演直接得 ${𝑡}_2:𝑇$；E-IfFalse 对称，反演得 ${𝑡}_3:𝑇$． 对 E-If，${𝑡}^{\prime }=\text{ if }{𝑡}_1^{\prime }\text{ then }{𝑡}_2\text{ else }{𝑡}_3$，前提为 ${𝑡}_1⟶{𝑡}_1^{\prime }$；反演得 ${𝑡}_1:\text{ Bool}$、${𝑡}_2:𝑇$、${𝑡}_3:𝑇$，对前提用 归纳假设 （取类型为 $\text{Bool}$）得 ${𝑡}_1^{\prime }:\text{ Bool}$，再用 T-If 即得结论． 对 E-PredZero，${𝑡}^{\prime }=0$，反演得 $𝑇=\text{ Nat}$，用 T-Zero． 对 E-PredSucc， t = pred (succ nv)， t' = nv，反演两次先得 $𝑇=\text{ Nat}$ 且 succ nv : Nat，再得 nv : Nat． 对 E-IsZeroZero 与 E-IsZeroSucc，${𝑡}^{\prime }$ 是 $\text{true}$ 或 $\text{false}$，反演得 $𝑇=\text{ Bool}$，用 T-True 或 T-False． 对同余规则 E-Succ，反演得 $𝑇=\text{ Nat}$ 且 ${𝑡}_1:\text{ Nat}$， 归纳假设 给出 ${𝑡}_1^{\prime }:\text{ Nat}$，再用 T-Succ；E-Pred 同理，最后用 T-Pred；E-IsZero 反演得 $𝑇=\text{ Bool}$ 且 ${𝑡}_1:\text{ Nat}$， 归纳假设 给出 ${𝑡}_1^{\prime }:\text{ Nat}$，最后用 T-IsZero．