A lambda abstraction does not support reference to the variable name in the applied expression, so x must be passed in as a parameter to x. We can think of this as replacing x by x x, but formally this is not correct. Instead defining y by \forall z, y\ z = x gives
