Lambda 演算 - 给出条件

Question

Give terms t1, t2, . . . , t5 such that the following derivation makes sense in the polymorphic lambda-calculus, where Γ = f : X → Y → Y, g : ∀Z.(Z → Z) → Z, x : X and X and Y are types.

我的答案如下

t1 = g Y

t2 = f x

t3 = f x t2

t4 = \y. f y t3

t5 = \g. \x. g (Z -> Z) (\z. z) x

我真的不确定这一点，我正在努力寻找可以帮助我验证这一点的材料。