That is, `(\x.y)z` reduces to `z`, but `\w.(\x.y)z` does not, because
the `\w` protects the redex in the body from reduction.
(A redex is a subform ...(\xM)N..., i.e., something that can be the
That is, `(\x.y)z` reduces to `z`, but `\w.(\x.y)z` does not, because
the `\w` protects the redex in the body from reduction.
(A redex is a subform ...(\xM)N..., i.e., something that can be the