It's pretty easy to reason about that particular example if you have a type system. In a simply typed language, "f f x" is just a type error, so it doesn't do anything. In the polymorphic lambda calculus, the typing will force f to either be the identity, meaning that "f f x = x", or it will be a constant function, so you just replace "f f" with the constant.