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.