一致性的证明

写 $n = h\;a_1 \cdots a_k$，其中 $h$ 不是应用。

若 $k = 0$，则 $n = h$ 是宇宙、$\Pi$、$\lambda$ 或变量，因为除应用之外只有这几种形状。由生成引理，变量属于 $\dom(\Gamma)$。

设 $k \ge 1$。由外向内对应用使用 $k$ 次生成引理，可知每个前缀 $h\;a_1 \cdots a_i$ 都可定型，特别地，从最内层的应用 $h\;a_1$ 得到：对某些 $y$、$A$ 和 $B$ 有 $\Gamma \vdash h : \tPi{y}{A}{B}$。现在考虑 $h$ 的形状。它不是 $\lambda$，否则 $h\;a_1$ 就是范式项 $n$ 内部的一个 $\beta$ 可归约式；它也不是宇宙或 $\Pi$：由生成引理，它的类型将可转换为某个宇宙，而由合流性，宇宙不可转换为 $\tPi{y}{A}{B}$。所以 $h$ 是某个变量 $x$，由生成引理它属于 $\dom(\Gamma)$，且 $\Gamma \vdash x : \tPi{y}{A}{B}$，这就是所需的 $C$。

假设 $\cdot \vdash t : \tPi{P}{\Sort{0}}{P}$。由强规范化，$t$ 归约到某个范式项 $n$；由类型保持性，$\cdot \vdash n : \tPi{P}{\Sort{0}}{P}$。我们两次使用引理 D.2，证明这样的 $n$ 不存在。

范式是一个 $\lambda$。 由引理 D.2，$n$ 是宇宙、$\Pi$、$\lambda$ 或中性项。

• 它不是中性项，因为其头部必须是空上下文中的变量，而空上下文没有变量。
• 它不是宇宙或 $\Pi$，因为生成引理将使 $\tPi{P}{\Sort{0}}{P}$ 可转换为某个宇宙，而合流性排除了这一点。

所以 $n = \tLam{x}{A}{s}$。由生成引理，对某个 $B$ 有 $x : A \vdash s : B$ 且 $\tPi{P}{\Sort{0}}{P} \conv \tPi{x}{A}{B}$。由合流性，$A \conv \Sort{0}$，并且对新鲜的 $z$ 有 $\subst{P}{P}{z} \conv \subst{B}{x}{z}$，即 $z \conv \subst{B}{x}{z}$。两边同时用 $x$ 替换 $z$，由引理 D.1 的 (c)，这保持可转换性，于是得到 $x \conv B$。体 $s$ 是范式，因为它是范式项 $n$ 的子项。简言之：$x : A \vdash s : B$，其中 $A \conv \Sort{0}$ 且 $B \conv x$。

这个体不可能存在。 令 $\Gamma = x : A$。由引理 D.2，$s$ 是宇宙、$\Pi$、$\lambda$ 或中性项。

• 若 $s$ 是宇宙或 $\Pi$，生成引理使 $B$ 可转换为某个宇宙；若 $s$ 是 $\lambda$，则使 $B$ 可转换为某个 $\Pi$。但 $B \conv x$，而由合流性，变量与两者都不可转换。
• 若 $s$ 是中性项，其头部是 $\dom(\Gamma) = \{x\}$ 中的变量，所以 $s = x\;a_1 \cdots a_k$。若 $k = 0$，则 $s = x$，生成引理给出 $B \conv A$。于是 $x \conv B \conv A \conv \Sort{0}$，但变量不可转换为宇宙。若 $k \ge 1$，引理 D.2 给出 $\Gamma \vdash x : C$，其中 $C$ 可转换为某个 $\Pi$，而对变量 $x$ 用生成引理得到 $C \conv A \conv \Sort{0}$。于是一个 $\Pi$ 可转换为一个宇宙，这被合流性排除。

每种情形都导出矛盾，所以没有闭项具有类型 $\tPi{P}{\Sort{0}}{P}$。