Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 1 / b / Solution

Write $I\equiv \lambda u.u$ for the I combinator, and choose $x$ outside the free variables of $p$. Both orders of composition of lambda terms first give the same lambda abstraction by beta reduction:The freshness condition is exactly the side condition for eta conversion, which contracts $\lambda x.px$ to $p$. ThereforeHere eta conversion matters: a free variable $p$ is already in beta-normal form, as is $\lambda x.px$, and beta equivalence alone does not equate them.