Does anyone have an idea how to prove in lambda calculus that bool contains two terms? I am quite new to it and I haven't succeeded in doing so. I came up with two terms so far, which would guarantee existence: $\lambda x_{\alpha}.\lambda y_{\alpha}.x$ and $\lambda x_{\alpha}.\lambda y_{\alpha}.y$. These terms are clearly of the type $Bool$.
But how can we prove that there are no other ones? I have tried induction on terms, induction on types, but everything failed so far. Any tips are welcome, thanks.
Your theorem statement has "atomic" carrying a decent load. You may want to consider what (if anything) about "atomic types" make this theorem true. In particular, you can "generalize" the statement.
At any rate, you want to do an induction on normal forms. The statement you want to prove can be formulated as $$\forall t\in \mathcal{N}. t\text{ has type } Bool\iff(t = \lambda x_\alpha.\lambda y_\alpha. x \lor t = \lambda x_\alpha.\lambda y_\alpha. y)$$ where $\mathcal{N}$ is the set of ($\alpha$-equivalence classes of) normal forms and (thus) equality, here, means $\alpha$-equivalence. $\mathcal{N}$ is roughly an inductively defined set and so to prove a statement about all its elements requires induction. However, since the terms include binding forms things get a bit hairier. In particular, and this will be a common move, you need to strengthen the induction hypothesis to hold for open terms. So instead of doing induction over normal forms, you want to do induction over "normal-forms-in-context". (We can simplify significantly for this particular problem [how?], but I will work more generally.) What's happening is that closed terms (and normal forms) do not form an inductively defined set (at least not in a natural way), but terms-in-context do.
Given a list of types called $\Gamma$, we can define $\mathtt{vars}(\Gamma)\equiv\{x^i\mid i < \#\Gamma\}$ to be a corresponding set of variables where $\#\Gamma$ is the length of $\Gamma$. Finally, define $$\alpha^\Gamma \equiv \begin{cases}\alpha, & \Gamma = \cdot\\\beta\to\alpha^\Delta, & \Gamma = \beta,\Delta\end{cases}$$ and $$\mathtt{abstract}(\Gamma,x)\equiv\begin{cases}x, &\Gamma = \cdot\\\lambda x^{\#\Delta}_\beta.\mathtt{abstract}(\Delta,x), & \Gamma = \beta,\Delta\end{cases}$$ The strengthened (but not quite correct) induction hypothesis is now $$\forall \Gamma.\forall t\in \mathcal{N}.\ \cdot\vdash t:\alpha^\Gamma\iff t \in\{\mathtt{abstract}(\Gamma,x)\mid x \in \mathtt{vars}(\Gamma)\land \Gamma\vdash x:\alpha\}$$ where $\Gamma\vdash t : \alpha$ means $t$ has type $\alpha$ in context $\Gamma$. As stated, this is not true, but if we restrict $\Gamma$ to lists of "atomic" types, it is. The original theorem is recovered in the $\alpha,\alpha,\cdot$ case.