Construct a proof tree in Hindley-Milner with function overload
After some time I realized that is not possible to proof 
\begin{align*}
\vdash (over\: eq:: Eq\: \alpha\: in\: inst\: eq :: Eq\:Int \:=\: eqInt\: in\: eq\:1\:2)::Bool
\end{align*}
 without suppositions about $1$, $2$ and $eqInt$ ( $\emptyset$ as the context). They need to be bound to the context , because they should be seen as build in
to the system. In alternative I could create new rules (like $const$ rules) for the integer numbers ($1$, $2$...) and for $eqInt$, that don't insert stuff to the context.

So, my final result is this proof tree:


I'm not sure if I can use $weakening$ in the context, but I did.

I hope that some one could comment something about my answer. If I'm right or if I created some non-sense.