%
\label{prop:well-ordering}
$(\Obj(\tau), <_\tau)$ is a well-ordering.
That is:
\begin{enumerate}
    \item $<_\tau$ is a strict total order on $\Obj(\tau)$.
    \item Every non-empty subset of $\Obj(\tau)$
          has a $<_\tau$-minimum element.
\end{enumerate}

\emph{Total order.}
$<_\tau$ is irreflexive (distinct seeds or distinct depths),
transitive (inherited from the generator order and $\mathbb{N}$),
and trichotomous (every two objects are comparable:
either their seeds differ, giving an order from $\KAxiom{1}$,
or their seeds agree and their depths are natural numbers,
giving an order from $\mathbb{N}$).

\emph{Well-ordering.}
Let $S \subseteq \Obj(\tau)$ be non-empty.
Among the seeds of elements in $S$,
let $g_0$ be the $\KAxiom{1}$-minimum.
Among elements of $S$ with seed $g_0$,
the minimum depth exists
(a non-empty subset of $\mathbb{N}$ has a minimum).
The corresponding element is the $<_\tau$-minimum of $S$.