Definition 5.4.2.  Let V ⊆ Var such that V is finite, T ∈ TV, x ∈ V, R ∈ TV ∖ {x}. We define
T[x:= R]
by:
(y)[x:= R] := {R if x = y(y) if x ≠ y  (y ∈ V)y. My)[x:= R] := λz. Mz[x:= R]  (My ∈ TV ∪ {y} for each y ∈ Fresh(V), [∀ y, z ∈ Fresh(V) : My[y:= z] = Mz])(MN)[x:= R] := M[x:= R] N[x:= R]  (M, N ∈ TV)
Remarks.

Note that we do not allow x to appear free in R. This ensures that x does not appear free in the result either, which is important for e.g. the definition $"beta reduction" of beta reduction.

References.