采用 类型与类型判断 的类型规则 和 一步规约 的求值规则． 取良类型的项 $𝑡=\text{ pred }\left(\text{if }\text{ false }\text{ then }0\text{ else }\text{ succ }0\right):\text{ Nat}$， 跟着 进展 的证明走一遍．

$𝑡$ 的推导最后一步是 T-Pred， 前提为 $\text{if }\text{ false }\text{ then }0\text{ else }\text{ succ }0:\text{ Nat}$，对这个子项用 归纳假设 ． 子项的推导最后一步是 T-If，前提里有 $\text{false }:\text{ Bool}$； $\text{false}$ 是值，由 典范形式 知它必为 $\text{true}$ 或 $\text{false}$， 这里恰好是 $\text{false}$，于是用 E-IfFalse 得子项 $⟶\text{ succ }0$． 回到整项 $𝑡$，由于子项能规约，用 E-Pred 即得 $𝑡⟶\text{ pred }\left(\text{succ }0\right)$．

这段证明在断定“能规约”的同时，直接构造出了这一步的推导． 对 $\text{pred }\left(\text{succ }0\right)$ 再用一次进展： 子项 $\text{succ }0$ 是值，由 典范形式 它是数值， 且形如 succ nv，于是用 E-PredSucc 得到 $0$． 对 $0$ 再用一次进展：它是值，停止．