Past exam of the computer science course of the University of Oxford / 2015 / Lambda calculus and types / 2 / c

Begin with the variable typing judgment $\{x:A\}\mapsto x:A$. Because $z$ is absent from this typing context, the lambda abstraction rule permits $z$ to have type $\star$:Assign the entire lambda application $yx$ type $\star$ using the universal typing axiom, without attempting to assign a function type to $y$. ThenAlthough $y$ is a free variable of the body, it is absent from its recorded typing context. Consequently the lambda abstraction rule allows any simple type $B$ for $y$. Abstract over $y$ and then $x$:The side condition for $y$ holds because $y$ is absent; the side condition for $x$ holds because its recorded simple type is $A$. Thus