Следствие 2

Если u = v₁ и u = v₂, причем v₁ и v₂ находятся в нф, то v₁ ≡_αv₂, т.е. равны с точностью до α-конверсии.

Доказательство

Согласно следствию 1 и транзитивности =, найдётся терм w такой, что v₁ → w и v₂ → w. Но так как v₁ и v₂ уже имеют нормальную форму, редукционные цепочки, приводящие к терму w, могут состоять лишь из α-конверсий.