Theorem. 类型唯一 Glomzzz 2026-10-10 About 对 类型与类型判断 的七条类型规则， 若 𝑡:𝑇 且 𝑡:𝑇 ′，则 𝑇=𝑇 ′．Proof.对 𝑡 结构归纳（ 归纳证明的写法 ），对 𝑇、𝑇 ′ 一般化． 当 𝑡 是常量、succ 𝑡 1、pred 𝑡 1 或 iszero 𝑡 1 时， 由 反演 ，类型由项的形状直接唯一确定为 Bool 或 Nat，所以 𝑇=𝑇 ′． 当 𝑡= if 𝑡 1 then 𝑡 2 else 𝑡 3 时， 由 反演 第 2 条得 𝑡 2:𝑇 且 𝑡 2:𝑇 ′； 𝑡 2 是直接子项，由 归纳假设 得 𝑇=𝑇 ′．∎
