对 [例] 多步归约到值 的归约链，按 [定义] 类型与类型判断 在每一项旁边写上类型。归约关系使用 [定义] 一步归约 ，保型性质及其证明见 [定理] 保型 ：

$$\begin{array}{cccc}& \text{ if }\left(\text{iszero }\left(\text{pred }\left(\text{succ }0\right)\right)\right)\text{ then }\text{ succ }0\text{ else }0& & :\text{ Nat }\\ ⟶& \text{ if }\left(\text{iszero }0\right)\text{ then }\text{ succ }0\text{ else }0& & :\text{ Nat }\\ ⟶& \text{ if }\text{ true }\text{ then }\text{ succ }0\text{ else }0& & :\text{ Nat }\\ ⟶& \text{ succ }0& & :\text{ Nat}\end{array}$$

类型始终是 $\text{Nat}$。以第一步为例看保型的证明怎样工作：这一步的推导是 E-If，前提是 $\text{iszero }\left(\text{pred }\left(\text{succ }0\right)\right)⟶\text{ iszero }0$。由 [引理] 反演 对 $𝑡:\text{ Nat}$ 反演，得到条件 $:\text{ Bool}$、两个分支 $:\text{ Nat}$；对前提用 归纳假设 （取类型 $\text{Bool}$），得到 $\text{iszero }0:\text{ Bool}$；两个分支原封不动，再用 T-If 拼回去，得到新项 $:\text{ Nat}$。

注意项本身变了很多，从一个 $\text{if}$ 变成了 $\text{succ }0$，但类型这个“静态描述”一直成立。保型说的就是：运行不会让类型说过的话失效。