A D62: Sequence $x : \mathbb{N} \to X$ is eventually constant if and only if \begin{equation} \exists \, a \in X : \exists \, N \in \mathbb{N} : \forall \, n \geq N : x_n = a \end{equation}