存在性。从 $𝑡$ 出发，只要有后继就继续归约。由 [引理] 归约使大小严格下降 ，每步大小严格下降，归约链至多有 $\mathrm{size}\left(𝑡\right)-1$ 步，因而必能到达一个没有后继的项 $𝑢$。由 [定理] 保型 对链长归纳，$𝑢:𝑇$。再用 [定理] 进展 ：$𝑢$ 是值或能归约，而后一种情况已被排除，所以 $𝑢$ 是具有类型 $𝑇$ 的值。

唯一性。设 $𝑡{⟶}^{\ast }𝑣$ 且 $𝑡{⟶}^{\ast }𝑤$，其中 $𝑣$、$𝑤$ 都是值。对第一条链的长度归纳；归纳性质允许第二条链任意长。

• 零步：$𝑡=𝑣$。由 [引理] 值不可归约 ，$𝑡$ 没有后继，因此第二条链也只能有零步，$𝑤=𝑡=𝑣$。
• 至少一步：第一条链形如 $𝑡⟶{𝑡}_1{⟶}^{\ast }𝑣$。$𝑡$ 能归约，故由 [引理] 值不可归约 它不是值；第二条链不能有零步，形如 $𝑡⟶{𝑡}_2{⟶}^{\ast }𝑤$。由 [定理] 确定性 ，${𝑡}_1={𝑡}_2$。两条剩余链从同一项出发，第一条的长度更小，由 归纳假设 得 $𝑣=𝑤$。