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

1. $𝑡$ 的推导最后一步是 T-Pred，前提 $\text{if }\text{ false }\text{ then }0\text{ else }\text{ succ }0:\text{ Nat}$。对这个子项用 归纳假设 。
2. 子项的推导最后一步是 T-If，前提里有 $\text{false }:\text{ Bool}$。$\text{false}$ 是值，由 [引理] 典范形式（canonical forms） 它是 $\text{true}$ 或 $\text{false}$，这里是 $\text{false}$，于是用 E-IfFalse：子项 $⟶\text{ succ }0$。
3. 回到 $𝑡$：子项能归约，所以用 E-Pred，$𝑡⟶\text{ pred }\left(\text{succ }0\right)$。

证明不只说“能归约”，还构造出了这一步的推导。对 $\text{pred }\left(\text{succ }0\right)$ 再用一次进展：子项 $\text{succ }0$ 是值，由 [引理] 典范形式（canonical forms） 它是数值，且形如 ，于是用 E-PredSucc 得到 $0$。对 $0$ 再用一次进展：它是值，停止。