%
\label{prop:tetration-injective}
For fixed $\underline{a} \geq \underline{2}$,
the map $\underline{c} \mapsto {}^{\underline{c}}\underline{a}$
is injective on $\tau$-Idx:
\[
    {}^{\underline{c_1}}\underline{a}
    = {}^{\underline{c_2}}\underline{a}
    \quad\Longrightarrow\quad
    \underline{c_1} = \underline{c_2}.
\]

We prove by induction on $\max(c_1, c_2)$
that the tetration function is strictly increasing
in the tower height $c$ (for fixed base $a \geq 2$),
from which injectivity follows.

\emph{Base case.}
${}^{\underline{0}}\underline{a} = \underline{1}$
and ${}^{\underline{1}}\underline{a} = \underline{a} \geq \underline{2}$.
So ${}^{\underline{0}}\underline{a} < {}^{\underline{1}}\underline{a}$.

\emph{Inductive step.}
Assume ${}^{\underline{c}}\underline{a}
< {}^{\underline{c+1}}\underline{a}$ for some $c$.
Then
${}^{\underline{c+2}}\underline{a}
= \underline{a}^{({}^{\underline{c+1}}\underline{a})}
> \underline{a}^{({}^{\underline{c}}\underline{a})}
= {}^{\underline{c+1}}\underline{a}$,
where the inequality uses the fact that
$x \mapsto \underline{a}^x$ is strictly increasing
for $\underline{a} \geq \underline{2}$.

Strict monotonicity implies injectivity.