Definition 5.4.1.  Let V ⊆ Var such that V is finite. We define:
TV:=: {(x) | x ∈ Vλx. Mx | Mx ∈ TV ∪ {x} for each x ∈ Fresh(V), [∀ x, y ∈ Fresh(V) : Mx[x:= y] = My]MN | M, N ∈ TV}
(x) = (y)  :⇔  x = y  (x ∈ V, y ∈ V)
λx. Mx = λx. M'x  :⇔  ∀ x ∈ Fresh(V) : Mx = M'x  (Mx ∈ TV ∪ {x} for each x ∈ Fresh(V), M'x ∈ TV ∪ {x} for each x ∈ Fresh(V) with suitable conditions)  ⇔  ∃ x ∈ Fresh(V) : Mx = M'x
MN = M'N'  :⇔  M = M' and N = N'  (M, N ∈ TV, M', N' ∈ TV)
V ⊆:TV viax = (x)
Well-definedness.  No proof.

This formalization of the untyped lambda calculus is fairly standard except for one aspect: The right side of a lambda abstraction depends on the value of the bound variable used to define it (which is kind of the point of bound variables). To prevent wild pseudo-terms that actually differ in nontrivial ways depending on the variable, there needs to be an additional substitutability constraint. Although substitution is defined later, we can use it in this case because we are applying it to subterms only (i.e. we are employing mutual induction).