In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

I am trying to infer the type and prove that this is well-typed:

let $f =\lambda x.x$ in $f f$

Obviously the $f$ is the identity function, so it's the same as

let $id =\lambda x.x$ in $id$ $id$

I am trying to use these rules to infer the type, going bottom-up:

First I am using (T-LET') and on the left-hand side it's easy to show that $\lambda x.x$ is of type $\alpha \rightarrow \alpha$.

However, I have a trouble with the right hand side. Can someone please help me how to finish this?

If I understand you question correctly, you are wondering how the typing judgment $f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \beta$ can be proved, where $\beta$ is some (yet unknown) type.

As we are dealing with an application, the only rule that applies is T-App, so we end up with the following (partial) typing derivation, where $\gamma$ is yet another (unknown) type.
$$ \dfrac{\dfrac{\dfrac{}{x : \alpha \vdash x : \alpha}}
{\vdash \lambda x.x : \alpha \to \alpha} \quad\quad
\dfrac{f : \forall \alpha.\alpha \to \alpha \vdash f : \gamma \to \beta \quad\quad f : \forall \alpha.\alpha \to \alpha \vdash f : \gamma}
{f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \beta}}
{\vdash let \; f = \lambda x.x \;\; in \;\; f\;f : \beta} $$

Now, to complete the two open branches of the derivation, the only possibility is to use the T-Var rule, which has two preconditions. Applying it in the left branch, you can easily see that $\gamma$ must actually be $\beta$. And similarly, applying the T-Var rule in the right branch, you learn that $\gamma$ (or rather $\beta$) must be an arrow type of the form $\delta \to \delta$. So in the end, you obtain the following derivation (omitting the "$f : \forall \alpha.\alpha\to\alpha \in f : \forall \alpha. \alpha \to \alpha$") for the second premise of the T-Let rule.
$$ \dfrac{\dfrac{\forall \alpha.\alpha\to\alpha \subseteq (\delta \to \delta) \to (\delta \to \delta)}{f : \forall \alpha.\alpha \to \alpha \vdash f : (\delta \to \delta) \to (\delta \to \delta)} \quad\quad \dfrac{\forall \alpha.\alpha\to\alpha \subseteq \delta \to \delta}{f : \forall \alpha.\alpha \to \alpha \vdash f : \delta \to \delta}}
{f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \delta \to \delta}$$

Note that the conclusion of the full derivation then becomes $\vdash let \; f = \lambda x.x \;\; in \;\; f\;f : \delta \to \delta$.

StackExchange Computer Science Q#92874, answer score: 6