Definition 5.4.4 (β reduction).  Let V ⊆ Var such that V is finite. We define:
βV:= {z. Mz) N → My[y:= N] : Mx ∈ TV ∪ {x} for each x ∈ Fresh(V), N ∈ TV, y ∈ Fresh(V)}
References.