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.