# Term of System F whose type-erasure is $2(2)$

If $2$ is the Church numeral $\lambda fx. f(f(x))$, then is there a closed term $t$ of System F of type $\forall \alpha ((\alpha \to \alpha) \to (\alpha \to \alpha))$ such that the type-erasure of $t$ is the untyped term $2(2)$?

$$T = \Lambda \alpha.\lambda f:\alpha\to\alpha. \lambda x:\alpha. f(f(x))$$
We can then search for a term $M$ of the form
$$M = \Lambda \alpha. T \tau_1 (T \tau_2)$$
and try to find types $\tau_1,\tau_2$, possibly depending on $\alpha$, such that $M : \forall \alpha. (\alpha\to\alpha)\to(\alpha\to\alpha)$. Surely $M$ becomes $2(2)$ after type erasure.
I'll leave finding $\tau_1,\tau_2$ as an exercise. Think about what is the type of $M$, and require it to be the wanted one: this provides $\tau_1$. After that, choose $\tau_2$ so that $M$ is well-typed.