It suffices to remark there is a subterm *f* *f* in a context where *f* is
bound to a lambda. Hence both occurrences of *f* must have the same type,
which is not possible since the type of the right occurrence should be the
domain of the (arrow) type of the other one.