Solution
= Solution
A closed beta-eta-long normal term of type $\sigma\to\sigma\to\sigma$ must have the form $\lambda x:\sigma.\lambda y:\sigma.t$, where the normal term $t:\sigma$ can only be $x$ or $y$: the pure calculus has no constants or other closed source of a value of the atomic type $\sigma$. Hence the only two beta-eta-equivalence classes are the <Church Boolean>[Church Booleans]
$$
\top=\lambda x.\lambda y.x,
\qquad
\bot=\lambda x.\lambda y.y.
$$