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

唯一性．设 $𝑡{⟶}^{\ast }𝑣$ 且 $𝑡{⟶}^{\ast }𝑤$，其中 $𝑣$、$𝑤$ 都是值． 对第一条链的长度归纳；归纳性质允许第二条链任意长． 若第一条链有零步，则 $𝑡=𝑣$．由 值不可规约 ，$𝑡$ 没有后继， 因此第二条链也只能有零步，$𝑤=𝑡=𝑣$． 若第一条链至少有一步，它形如 $𝑡⟶{𝑡}_1{⟶}^{\ast }𝑣$． $𝑡$ 能规约，由 值不可规约 知它不属于值； 第二条链不能有零步，必形如 $𝑡⟶{𝑡}_2{⟶}^{\ast }𝑤$． 由 确定性 得 ${𝑡}_1={𝑡}_2$． 两条剩余链从同一项出发，第一条的长度更小，由 归纳假设 得 $𝑣=𝑤$．