Случай 1a также можно переписать как
y[x:=N] ≡ N, if x ≡ y
x, y, z, ... - это просто метапеременные, которые обозначают конкретные переменные u, v, w, ... на языке лямбда-исчисление. В принципе, мы могли бы вставить одну и ту же фактическую переменную для заполнителей x и y при применении шаблона определения к некоторому конкретному лямбда-термину, и это тот случай, когда x ≡ y.
1a охватывает случай, когда переменная в при которой происходит подстановка, такая же, как и при подстановке, а 1b охватывает случай, когда переменная, в которой происходит подстановка, не является той, которая заменяется. В случае 1a заменяется вся переменная; в случае 1b ничего не происходит.
Пример:
(a) (λu.u)(λw.w) >> u[u:=(λw.w)] ≡ (λw.w) (covered by case 1a)
(b) (λu.v)(λw.w) >> v[u:=(λw.w)] ≡ v (covered by case 1b)
Обе замены имеют вид y[x:=N], а в обоих примерах - N ≡ (λw.w). В (a), y ≡ u и x ≡ u, поэтому x ≡ y: это случай 1a. В (b), y ≡ v и x ≡ u, поэтому x \≡ y: это случай 1b.