对 多步规约到值 的规约链， 按 类型与类型判断 在每一项旁边写上类型． 规约关系使用 一步规约 ， 保型性质及其证明见 保型 ：

$$\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$，但类型这一静态描述一直成立． 保型说的就是：运行不会让类型作出的保证失效．