这里的四条结论只针对 类型与类型判断 的七条类型规则； $𝑡:𝑇$ 表示能由这些规则搭出有限推导，$\text{Bool}$、$\text{Nat}$ 分别是布尔类型与自然数类型． 第 1 条，若 $\text{true }:𝑇$ 或 $\text{false }:𝑇$，则 $𝑇=\text{ Bool}$；若 $0:𝑇$，则 $𝑇=\text{ Nat}$． 第 2 条，若 $\text{if }{𝑡}_1\text{ then }{𝑡}_2\text{ else }{𝑡}_3:𝑇$，则 ${𝑡}_1:\text{ Bool}$，${𝑡}_2:𝑇$，${𝑡}_3:𝑇$． 第 3 条，若 $\text{succ }{𝑡}_1:𝑇$ 或 $\text{pred }{𝑡}_1:𝑇$，则 $𝑇=\text{ Nat}$ 且 ${𝑡}_1:\text{ Nat}$． 第 4 条，若 $\text{iszero }{𝑡}_1:𝑇$，则 $𝑇=\text{ Bool}$ 且 ${𝑡}_1:\text{ Nat}$．