How to prove that these are the only type inhabitants? Consider a type $$\mathsf{Boolean} = \forall \alpha.\ \alpha \to \alpha \to \alpha$$
with its two inhabitants
\begin{align}
\mathrm{tt} &= \lambda x.\ \lambda y.\ x \\
\mathrm{ff} &= \lambda x.\ \lambda y.\ y
\end{align}
or using System-F notation
\begin{align}
\mathrm{tt} &= \Lambda \alpha.\ \lambda x:\alpha.\ \lambda y:\alpha.\ x \\
\mathrm{ff} &= \Lambda \alpha.\ \lambda x:\alpha.\ \lambda y:\alpha.\ y
\end{align}
I would like to prove that these are the only inhabitants of $\mathsf{Boolean}$. Of course, there have to be some additional assumptions which exclude functions like
$$\mathrm{if\_boolean} = \Lambda \alpha.\ \lambda x:\alpha.\ \lambda y:\alpha.\ \begin{cases} x& \text{ if }\alpha = \mathsf{Boolean}\\y &\text{ otherwise}\end{cases}$$
but I don't know how to formalize it. 
Do you know how to formalize and prove it?
I would appreciate any help, ideas or references.

This is a consequence of the parametricity theorem. Two references for further information are at the end of this answer, but informally, the parametricity theorem states that type substitutions commute with polymorphic functions.
In your case, the parametricity theorem states that any function with this type:
$$\hbox{boolean} : \forall \alpha. \alpha \rightarrow \alpha \rightarrow \alpha$$
must satisfy the following theorem. If $A$ and $B$ are types, and $R$ is any relation between elements of $A$ and $B$, then:
$$\forall (x,p) \in R, (y,q) \in R. (\hbox{boolean}\,A\,x\,y,\hbox{boolean}\,B\,p\,q) \in R$$
This has a number of useful consequences. For example, if $R$ is a function, it says that for all types $A$ and $B$:
$$\forall f : A \rightarrow B. \forall x, y : A. f\,(\hbox{boolean}\,A\,x\,y) = \hbox{boolean}\,B\,(f\,x)\,(f\,y)$$
But in our case, it's even simpler. Let $A$ be the set $\{\mathbf{a}_1, \mathbf{a}_2\}$ and  $B$ be the set $\{\mathbf{b}_1, \mathbf{b}_2\}$. Define a relation $R$ to be $\{(\mathbf{a}_1,\mathbf{b}_1), (\mathbf{a}_2,\mathbf{b}_2)\}$. Then this means that:
$$(\hbox{boolean}\,A\,\mathbf{a}_1\,\mathbf{a}_2, \hbox{boolean}\,B\,\mathbf{b}_1\,\mathbf{b}_2) \in R$$
But there are only two elements of $R$. Therefore, either:
$$\hbox{boolean}\,A\,\mathbf{a}_1\,\mathbf{a}_2 = \mathbf{a}_1 \wedge \hbox{boolean}\,B\,\mathbf{b}_1\,\mathbf{b}_2 = \mathbf{b}_1$$
or:
$$\hbox{boolean}\,A\,\mathbf{a}_1\,\mathbf{a}_2 = \mathbf{a}_2 \wedge \hbox{boolean}\,B\,\mathbf{b}_1\,\mathbf{b}_2 = \mathbf{b}_2$$
It follows that $\hbox{boolean}$ must be either $\hbox{tt}$ or $\hbox{ff}$.
I haven't tried it, but you might also want to consider using the Girard-Reynolds isomorphism, and show that there are only two normalised proofs of the Reynolds embedding of the type of $\hbox{boolean}$.

Reynolds, J.C. (1983). "Types, abstraction, and parametric polymorphism". Information Processing. North Holland, Amsterdam. pp. 513–523. http://www.cse.chalmers.se/edu/year/2010/course/DAT140_Types/Reynolds_typesabpara.pdf (Wayback Machine)
Wadler, Philip (September 1989). "Theorems for free!". 4th Int'l Conf. on Functional Programming and Computer Architecture. London. https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.38.9875
