# Is it true that if $M : \forall \alpha . \left( \alpha \rightarrow \alpha \right)$ is a closed term then $M = \Lambda \alpha. \lambda x^{\alpha} . x$?

In system F, is every closed term $$M$$, which is of $$\forall \alpha . \left( \alpha \rightarrow \alpha \right)$$, $$\alpha \beta \eta$$-equivalent to $$\Lambda \alpha. \lambda x^{\alpha} . x$$?

I have believed that this is true and have tried to prove it by using the equation

$$\forall \alpha. \forall \beta. \forall f^{\alpha \rightarrow \beta} . \forall x^{\alpha} . M \beta \left( f x \right) = f \left( M \alpha x \right)$$

, which I think is a consequence of theorems for Free, but couldn't prove it.

• Let $y : \beta$ be arbitrary, and replace $f$ with $\lambda z^{\alpha} . y$. Then $M \beta y = y$. – 임기정 Feb 15 at 4:30