由 值与数值 ， 值只有三种形状：$\text{true}$、$\text{false}$、数值． 对第 1 条，若 $𝑣$ 是数值，它是 $0$（由 反演 第 1 条，类型只能是 $\text{Nat}$）或 succ nv（由第 3 条，类型只能是 $\text{Nat}$）；由 类型唯一 ，它不可能同时具有类型 $\text{Bool}$，所以类型为 $\text{Bool}$ 的值只能是 $\text{true}$ 或 $\text{false}$． 对第 2 条，由 反演 第 1 条，$\text{true}$、$\text{false}$ 的类型只能是 $\text{Bool}$，所以类型为 $\text{Nat}$ 的值只能是数值．