Reasoning:
The definition of f is equivalent to
f = x |→ (y |→ (z |→ x [y::z])).Suppose tx is the type of x, ty is the type of y, tz is the type of z, and t is the type of expression (x [y::z]). Then the type of f is tx → ty → tz → t.
Suppose ty = α The presence of expression y::z means that tz = [α]. So [y::z] has type [[α]].
Notice that x is being applied. So it is a function. It takes parameter [y::z], of type [[α]]. So the domain of tx is [[α]].
The codomain of tx is the type of the right-hand side of the equation, called t above, which is also the type of the codomain of f. There are no constraints on that type, so call it β. That means tx = [[α]] → β.
Substituting the values of tx, ty, tz and t into the type of f gives the answer.