以下结论只针对 [定义] 类型与类型判断 的七条类型规则；$𝑡:𝑇$ 表示能由这些规则搭出有限推导，$\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}$。