%
\label{lem:tail-agreement-propagation}
Let $T, S \in \mathrm{HolFun}$.
If $T$ and $S$ agree at depth $d_0$
(Definition~\ref{def:tail-agreement}),
then they agree at \emph{all} depths.
That is:
\[
    \boxed{%
    T \sim_{d_0} S
    \;\;\Longrightarrow\;\;
    \forall\, d \geq 1,\;
    \forall\, t \text{ with } \mathrm{depth}(t) \geq d,\;
    \forall\, k \leq d:\;
    \bigl(T(t)\bigr)_k = \bigl(S(t)\bigr)_k.}
\]

By induction on $d$, starting from $d_0$.

\textbf{Base case} ($d = d_0$):
this is the hypothesis $T \sim_{d_0} S$.

\textbf{Induction step} ($d \to d + 1$):
assume $T$ and $S$ agree at depth $d$.
We show they agree at depth $d + 1$.
Take any omega-tail $t$ of depth $\geq d + 1$.

At primorial stage $M_{d+1} = M_d \cdot p_{d+1}$,
the Chinese Remainder Theorem gives the decomposition:
\[
    \mathbb{Z}/M_{d+1}\mathbb{Z}
    \;\cong\;
    \mathbb{Z}/M_d\mathbb{Z}
    \;\times\;
    \mathbb{Z}/p_{d+1}\mathbb{Z}.
\]

By the induction hypothesis,
$T(t)$ and $S(t)$ agree on the
$\mathbb{Z}/M_d\mathbb{Z}$ factor:
for all $k \leq d$,
$\bigl(T(t)\bigr)_k = \bigl(S(t)\bigr)_k$.

It remains to show agreement
on the $\mathbb{Z}/p_{d+1}\mathbb{Z}$ factor.
Tower coherence
(Definition~\ref{def:tower-coherence}, I.D46)
gives:
\[
    T(t) \bmod M_d \;=\; T(t \bmod M_d),
    \qquad
    S(t) \bmod M_d \;=\; S(t \bmod M_d).
\]
The reduction $t \bmod M_d$
is an omega-tail of depth $d$.
By the induction hypothesis,
$T(t \bmod M_d) = S(t \bmod M_d)$
at all components $k \leq d$.

Now the CRT coherence constraint
(Theorem~\ref{thm:crt-coherence}, I.T18)
enters.
A HolFun's action on $\mathbb{Z}/M_{d+1}\mathbb{Z}$
is determined by its actions on the two CRT factors
$\mathbb{Z}/M_d\mathbb{Z}$ and $\mathbb{Z}/p_{d+1}\mathbb{Z}$.
The CRT coherence condition requires
that the $p_{d+1}$-factor of the output
is consistent with the already-determined lower stages:
the action on $\mathbb{Z}/p_{d+1}\mathbb{Z}$
is constrained by the requirement
that the full CRT reconstruction
at stage $M_{d+1}$
must be compatible with the tower reduction
to stage $M_d$.
Since $T$ and $S$ agree on the $\mathbb{Z}/M_d\mathbb{Z}$ factor,
and both satisfy CRT coherence,
the $p_{d+1}$-factor of $T(t)$ and $S(t)$
must agree as well ---
because any discrepancy on the $p_{d+1}$-factor
would violate the CRT coherence constraint
for the tower reduction
$M_{d+1} \to M_d$.

Therefore $\bigl(T(t)\bigr)_{d+1} = \bigl(S(t)\bigr)_{d+1}$,
completing the induction.