Definition 5.4.5 (η conversion).  Let V ⊆ Var such that V is finite. We define:
ηV:= {λz. Mz → M : M ∈ TV}
References.