f x is a function. It is the function (y |-> (x+1)::y).