by $\alpha$-conversion. By Lemma 4, there exist family contexts $\Psi_{0}$,
$(\Psi_{i})_{i\in I}$, typing contexts $\Delta_{0}$, $(\Delta_{i})_{i\in I}$,
multi-counters $\mathfrak{n}_{0}$, $(\mathfrak{n}_{i})_{i\in I}$ and
multitypes $\mathcal{S}_{0}$, $(\mathcal{S}_{i})_{i\in I}$ such that
$\Psi=\Psi_{0}+_{i\in I}\Psi_{i}$ and $\Delta=\Delta_{0}+_{i\in I}\Delta_{i}$
and $\mathfrak{n}=\mathfrak{n}_{0}+_{i\in I}\mathfrak{n}_{i}$ and such that
$\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}\mathbf{v}:\mathcal{S}_{i}$
and $\mathcal{S}^{?}_{i}\lhd\mathcal{S}_{i}$ for each $i\in\\{0\\}\cup I$. By
IH on $\pi_{0}$ with $\zeta_{0}$ and $\pi_{i}$ with $\zeta_{i}$ for each
${i\in I}$, we have
$\pi^{\prime}_{0}\rhd(\Phi_{0},y:\\{\\!\\!\\{\mathcal{U}_{i}\\}\\!\\!\\}_{i\in
I})+\Psi_{0};\Gamma_{0}+\Delta_{0}\vdash^{\mathfrak{m}_{0}+\mathfrak{n}_{0}}s\\{x:=\mathbf{v}\\}:\mathcal{T}$
and
$\pi^{\prime}_{i}\rhd\Phi_{i}+\Psi_{i};\Gamma_{i}+\Delta_{i}\vdash^{\mathfrak{m}_{i}+\mathfrak{n}_{i}}\mathsf{fix}\,y.\,s\\{x:=\mathbf{v}\\}:\mathcal{U}_{i}$
for each ${i\in I}$. By Lemma 2 and $\alpha$-conversion we can write
$(\Phi_{0},y:\\{\\!\\!\\{\mathcal{U}_{i}\\}\\!\\!\\}_{i\in I})+\Psi_{0}$ as
$\Phi_{0}+\Psi_{0},y:\\{\\!\\!\\{\mathcal{U}_{i}\\}\\!\\!\\}_{i\in I}$.
Applying rule t-fix with $\pi^{\prime}_{0}$ and $(\pi^{\prime}_{i})_{i\in I}$
as premises, we conclude with
$\pi^{\prime}\rhd\Phi+\Psi;\Gamma+\Delta\vdash^{\mathfrak{m}+\mathfrak{n}}\mathsf{fix}\,y.\,s\\{x:=\mathbf{v}\\}:\mathcal{T}$,
and we are done since
$\mathsf{fix}\,y.\,s\\{x:=\mathbf{v}\\}=(\mathsf{fix}\,y.\,s)\\{x:=\mathbf{v}\\}$

∎

*

###### Proof.

We proceed by induction on $\pi$.

  1. 1.

t-var1. Then $\pi\rhd\varnothing;y:\mathcal{T}\vdash^{[\,]}y:\mathcal{T}$,
where $\Phi,x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I}=\varnothing$
and $\Gamma=y:\mathcal{T}$ and $\mathfrak{m}=[\,]$ and $t=y$. By the invariant
we have $x\neq y$, hence $I=\varnothing$. We conclude by letting
$\pi^{\prime}:=\pi$.

  2. 2.

t-var2. Then $\pi\rhd
y:\\{\\!\\!\\{\mathcal{T}\\}\\!\\!\\};\varnothing\vdash^{[\,]}y:\mathcal{T}$,
where $(\Phi,x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I})=y:\\{\\!\\!\\{\mathcal{T}\\}\\!\\!\\}$ and $\Gamma=\varnothing$,
$\mathfrak{m}=[\,]$ and $t=y$. We consider two subcases, depending on whether
$x=y$ or not:

    1. 2.1

If $x=y$, then $\Phi=\varnothing$ and
$\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I}=\\{\\!\\!\\{\mathcal{T}\\}\\!\\!\\}$, i.e. $I$ is a singleton, so we have
only one judgment of the form $\Psi;\Delta\vdash^{\mathfrak{n}}q:\mathcal{S}$
and $\mathcal{S}=\mathcal{T}$. We conclude by letting $\pi^{\prime}:=\zeta$.

    2. 2.2

If $x\neq y$, then $\Phi=y:\\{\\!\\!\\{\mathcal{T}\\}\\!\\!\\}$ and
$\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I}=\\{\\!\\!\\{\,\\}\\!\\!\\}$,
that is, $I=\varnothing$. We conclude by letting $\pi^{\prime}:=\pi$.

  3. 3.

t-abs. Then $\pi\rhd+_{j\in J}\Phi_{j},x:+_{j\in
J}\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I_{j}};+_{j\in
J}\Gamma_{j}\vdash^{+_{j\in J}\mathfrak{m}_{j}}\lambda
y.\,s:[\mathcal{U}^{?}_{j}\to\mathcal{R}_{j}]^{\mathsf{abs}}_{j\in J}$, where
$\Phi=+_{j\in J}\Phi_{j}$ and $\Gamma=+_{j\in J}\Gamma_{j}$ and
$\mathfrak{m}=+_{j\in J}\mathfrak{m}_{j}$ and $t=\lambda y.\,s$ and
$\mathcal{T}=[\mathcal{U}^{?}_{j}\to\mathcal{R}_{j}]^{\mathsf{abs}}_{j\in J}$
and we can write $I$ as $\uplus_{j\in J}(I_{j})_{j\in J}$ so that
$\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I}=+_{j\in
J}\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I_{j}}$. The judgment is
derived from premises of the form
$\pi_{j}\rhd\Phi_{j},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I_{j}};\Gamma_{j},y:\mathcal{U}^{?}_{j}\vdash^{\mathfrak{m}_{j}}s:\mathcal{R}_{j}$
for each ${j\in J}$. Then for all ${j\in J}$ we can apply the IH on $\pi_{j}$
with $\zeta_{i}$ for all $i\in I_{j}$, yielding
$(\pi^{\prime}_{j}\rhd\Phi_{j}+_{i\in
I_{j}}\Psi_{i};(\Gamma_{j},y:\mathcal{U}^{?}_{j})+_{i\in
I_{j}}\Delta_{i}\vdash^{\mathfrak{m}_{j}+_{i\in
I_{j}}\mathfrak{n}_{i}}s\\{x:=q\\}:\mathcal{R}_{j})_{j\in J}$. By Lemma 2 and
$\alpha$-conversion we can write $(\Gamma_{j},y:\mathcal{U}^{?}_{j})+_{i\in
I_{j}}\Delta_{i}$ as $\Gamma_{j}+_{i\in
I_{j}}\Delta_{i},y:\mathcal{U}^{?}_{j}$. We conclude
$\pi^{\prime}\rhd\Phi+_{i\in I}\Psi_{i};\Gamma+_{i\in
I}\Delta_{i}\vdash^{\mathfrak{m}+_{i\in I}\mathfrak{n}_{i}}\lambda
y.\,s\\{x:=q\\}:[\mathcal{U}^{?}_{j}\to\mathcal{R}_{j}]^{\mathsf{abs}}_{j\in
J}$. by applying rule t-abs to $(\pi^{\prime}_{j})_{j\in J}$, and we are done
since $\lambda y.\,s\\{x:=\mathbf{v}\\}=(\lambda y.\,s)\\{x:=\mathbf{v}\\}$.

  4. 4.

t-app. Then
$\pi\rhd\Phi_{1}+\Phi_{2},x:\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J}+\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in
K};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}s\,u:\mathcal{T}$,
where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and $t=s\,u$,
and we can write $I$ as $J\uplus K$ so that
$\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I}=\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J}+\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in K}$. The judgment is derived
from $\pi_{1}\rhd\Phi_{1},x:\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathcal{U}^{?}\to\mathcal{T}]^{\mathsf{abs}}$
and $\pi_{2}\rhd\Phi_{2},x:\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in
K};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}u:\mathcal{U}$, where (1)
$\mathcal{U}^{?}\lhd\mathcal{U}$. We can apply IH on $\pi_{1}$ and
$(\zeta_{j})_{j\in J}$, yielding $\pi^{\prime}_{1}\rhd\Phi_{1}+_{j\in
J}\Psi_{j};\Gamma_{1}+_{j\in J}\Delta_{j}\vdash^{\mathfrak{m}_{1}+_{j\in
J}\mathfrak{n}_{j}}s\\{x:=q\\}:[\mathcal{U}^{?}\to\mathcal{T}]^{\mathsf{abs}}$.
On the other hand, we can apply IH on $\pi_{2}$ and $(\zeta_{k})_{k\in K}$,
yielding $\pi^{\prime}_{2}\rhd\Phi_{2}+_{k\in K}\Psi_{k};\Gamma_{2}+_{k\in
K}\Delta_{k}\vdash^{\mathfrak{m}_{2}+_{k\in
K}\mathfrak{n}_{k}}u\\{x:=q\\}:\mathcal{U}$. Applying rule t-app with
$\pi^{\prime}_{1}$, $\pi^{\prime}_{2}$, and (1) as premises we conclude with
$\pi^{\prime}\rhd\Phi+_{i\in I}\Psi_{i};\Gamma+_{i\in
I}\Delta_{i}\vdash^{\mathfrak{m}+_{i\in
I}\mathfrak{n}_{i}}s\\{x:=q\\}\,u\\{x:=q\\}:\mathcal{T}$, and we are done
since $s\\{x:=q\\}\,u\\{x:=q\\}=(s\,u)\\{x:=q\\}$.

  5. 5.

t-zero. Then $\pi\rhd\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\mathbb{0}]^{\mathsf{nat}}_{j\in J}$, where
$\Phi,x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I}=\varnothing$ and
$\Gamma=\varnothing$ and $\mathfrak{m}=[\,]$ and $t={\bf 0}$ and
$\mathcal{T}=[\mathbb{0}]^{\mathsf{nat}}_{j\in J}$. Hence
$\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I}=\\{\\!\\!\\{\,\\}\\!\\!\\}$,
then $I=\varnothing$. We conclude by letting $\pi^{\prime}:=\pi$, since ${\bf
0}\\{x:=q\\}={\bf 0}$.

  6. 6.

t-succ. Then $\pi\rhd\Phi,x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(u):[\mathbb{S}(\mathcal{N}_{j})]^{\mathsf{nat}}_{j\in
J}$, where $t=\mathbf{S}(u)$ and
$\mathcal{T}=[\mathbb{S}(\mathcal{N}_{j})]^{\mathsf{nat}}_{j\in J}$. The
judgment is derived from
$\pi_{0}\rhd\Phi,x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma\vdash^{\mathfrak{m}}u:+_{j\in J}\mathcal{N}_{j}$. We can apply IH on
$\pi_{0}$ with $(\zeta_{i})_{i\in I}$, yielding
$\pi^{\prime}_{0}\rhd\Phi+_{i\in I}\Psi_{i};\Gamma+_{i\in
I}\Delta_{i}\vdash^{\mathfrak{m}+_{i\in I}\mathfrak{n}_{i}}u\\{x:=q\\}:+_{j\in
J}\mathcal{N}_{j}$. Applying rule t-succ, we conclude with
$\pi^{\prime}\rhd\Phi+_{i\in I}\Psi_{i};\Gamma+_{i\in
I}\Delta_{i}\vdash^{\mathfrak{m}+_{i\in
I}\mathfrak{n}_{i}}\mathbf{S}(u\\{x:=q\\}):[\mathbb{S}(\mathcal{N}_{j})]^{\mathsf{nat}}_{j\in
J}$, and we are done since
$\mathbf{S}(u\\{x:=q\\})=(\mathbf{S}(u))\\{x:=q\\}$.

  7. 7.

t-ifZero. Then
$\pi\rhd\Phi_{1}+\Phi_{2},x:\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J}+\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{k\in
K};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{I0}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}\mathsf{if}(s,u,y.\,r):\mathcal{T}$
where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\texttt{I0}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$t=\mathsf{if}(s,u,y.\,r)$, and $I=J\uplus K$ so that
$\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I}=\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J}+\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in K}$. The judgment is derived
from $\pi_{1}\rhd\Phi_{1},x:\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathbb{0}]^{\mathsf{nat}}$ and
$\pi_{2}\rhd\Phi_{2},x:\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in
K};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}u:\mathcal{T}$. By $\alpha$-conversion
we may assume $y\notin\\{x\\}\cup\mathsf{fv}(q)$. By IH on both $\pi_{1}$ with
$(\zeta_{j})_{j\in J}$ and $\pi_{2}$ with $(\pi_{k})_{k\in K}$ we have
$\pi^{\prime}_{1}\rhd\Phi_{1}+_{j\in J}\Psi_{j};\Gamma_{1}+_{j\in
J}\Delta_{j}\vdash^{\mathfrak{m}_{1}+_{j\in
J}\mathfrak{n}_{j}}s\\{x:=q\\}:[\mathbb{0}]^{\mathsf{nat}}$ and
$\pi^{\prime}_{2}\rhd\Phi_{2}+_{k\in K}\Psi_{k};\Gamma_{2}+_{k\in
K}\Delta_{k}\vdash^{\mathfrak{m}_{2}+_{k\in
K}\mathfrak{n}_{k}}u\\{x:=q\\}:\mathcal{T}$. Applying rule t-ifZero, we
conclude with $\pi^{\prime}\rhd\Phi+_{i\in I}\Psi;\Gamma+_{i\in
I}\Delta_{i}\vdash^{\mathfrak{m}+_{i\in
I}\mathfrak{n}_{i}}\mathsf{if}(s\\{x:=q\\},u\\{x:=q\\},y.\,r\\{x:=q\\}):\mathcal{T}$,
and we are done since
$\mathsf{if}(s\\{x:=q\\},u\\{x:=q\\},y.\,r\\{x:=q\\})=(\mathsf{if}(s,u,y.\,r))\\{x:=q\\}$.

  8. 8.

t-ifSucc. Then
$\pi\rhd\Phi_{1}+\Phi_{2}+x:\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J}+\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in
K};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{IS}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}\mathsf{if}(s,u,y.\,r):\mathcal{T}$
where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\texttt{IS}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$t=\mathsf{if}(s,u,y.\,r)$, and $I=J\uplus K$, so that
$\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I}=\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J}+\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in K}$. The judgment is derived
from $\pi_{1}\rhd\Phi_{1},x:\\{\\!\\!\\{\mathcal{S}_{j}\\}\\!\\!\\}_{j\in
J};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$
and $\pi_{2}\rhd\Phi_{2},x:\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in
K};\Gamma_{2},y:\mathcal{N}^{?}\vdash^{\mathfrak{m}_{2}}r:\mathcal{T}$ and (1)
$\mathcal{N}^{?}\lhd\mathcal{N}$. By $\alpha$-conversion we may assume
$y\notin\\{x\\}\cup\mathsf{fv}(q)$. Then by the IH on both $\pi_{1}$ with
$(\zeta_{j})_{j\in J}$ and $\pi_{2}$ with $(\zeta_{k})_{k\in K}$ we have
$\pi^{\prime}_{1}\rhd\Phi_{1}+_{j\in J}\Psi_{j};\Gamma_{1}+_{j\in
J}\Delta_{j}\vdash^{\mathfrak{m}_{1}+_{j\in
J}\mathfrak{n}_{j}}s\\{x:=q\\}:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$ and
$\pi^{\prime}_{2}\rhd\Phi_{2}+_{k\in
K}\Psi_{k};(\Gamma_{2},y:\mathcal{N}^{?})+_{k\in
K}\Delta_{k}\vdash^{\mathfrak{m}_{2}+_{k\in
K}\mathfrak{n}_{k}}r\\{x:=q\\}:\mathcal{T}$. By Lemma 2 and
$\alpha$-conversion we can write $(\Gamma_{2},y:\mathcal{N}^{?})+_{k\in
K}\Delta_{k}$ as $\Gamma_{2}+_{k\in K}\Delta_{k},y:\mathcal{N}^{?}$. Applying
rule t-ifSucc with $\pi^{\prime}_{1}$, $\pi^{\prime}_{2}$ and (1) as premises
we conclude with $\pi^{\prime}\rhd\Phi+_{i\in I}\Psi_{i};\Gamma+_{i\in
I}\Delta_{i}\vdash^{\mathfrak{m}+_{i\in
I}\mathfrak{n}_{i}}\mathsf{if}(s\\{x:=q\\},u\\{x:=q\\},y.\,r\\{x:=q\\}):\mathcal{T}$.

  9. 9.

t-fix. Then $\pi\rhd\Phi_{0}+_{j\in
J}\Phi_{j},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I_{0}}+_{j\in
J}\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I_{j}};\Gamma_{0}+_{j\in
J}\Gamma_{j}\vdash^{[\texttt{F}]+\mathfrak{m}_{0}+_{j\in
J}\mathfrak{m}_{j}}\mathsf{fix}\,y.\,s:\mathcal{T}$ where
$\Phi=\Phi_{0}+_{j\in J}\Phi_{j}$ and $\Gamma=\Gamma_{0}+_{j\in J}\Gamma_{j}$
and $\mathfrak{m}=[\texttt{F}]+\mathfrak{m}_{0}+_{j\in J}\mathfrak{m}_{j}$ and
$t=\mathsf{fix}\,y.\,s$, and we can write $I=I_{0}\uplus_{j\in J}I_{j}$, so
that $\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I}=\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I_{0}}+_{j\in
J}\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in I_{j}}$. The judgment is
derived from
$\pi_{0}\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I_{0}},y:\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in
J};\Gamma_{0}\vdash^{\mathfrak{m}_{0}}s:\mathcal{T}$ and
$\pi_{j}\rhd\Phi_{j},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I_{j}};\Gamma_{j}\vdash^{\mathfrak{m}_{j}}\mathsf{fix}\,y.\,s:\mathcal{U}_{j}$
for each ${j\in J}$. By $\alpha$-conversion we may assume
$y\notin\\{x\\}\cup\mathsf{fv}(q)$. Then by the IH on $\pi_{0}$ with
$(\zeta_{i})_{i\in I_{0}}$ and $(\pi_{j})_{j\in J}$ with $(\zeta_{i})_{i\in
I_{j}}$ we have
$\pi^{\prime}_{0}\rhd(\Phi_{0},y:\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in
J})+_{i\in I_{0}}\Psi_{i};\Gamma_{0}+_{i\in
I_{0}}\Delta_{i}\vdash^{\mathfrak{m}_{0}+_{i\in
I_{0}}\mathfrak{n}_{i}}s\\{x:=q\\}:\mathcal{T}$ and
$\pi^{\prime}_{j}\rhd\Phi_{j}+_{i\in I_{j}}\Psi_{i};\Gamma_{j}+_{i\in
I_{j}}\Delta_{i}\vdash^{\mathfrak{m}_{j}+_{i\in
I_{j}}\mathfrak{n}_{i}}(\mathsf{fix}\,y.\,s)\\{x:=q\\}:\mathcal{U}_{j}$ for
each ${j\in J}$, with
$(\mathsf{fix}\,y.\,s)\\{x:=q\\}=\mathsf{fix}\,y.\,s\\{x:=q\\}$. By Lemma 2
and $\alpha$-conversion we can write
$(\Phi_{0},y:\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in J})+_{i\in
I_{0}}\Psi_{i}$ as $\Phi_{0}+_{i\in
I_{0}}\Psi_{i},y:\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in J}$. Applying
rule t-fix we conclude with $\pi^{\prime}\rhd\Phi+_{i\in
I}\Psi_{i};\Gamma+_{i\in I}\Delta_{i}\vdash^{\mathfrak{m}+_{i\in
I}\mathfrak{n}_{i}}\mathsf{fix}\,y.\,s\\{x:=q\\}:\mathcal{T}$.

∎

*

###### Proof.

By induction on the derivation of $t\to_{\rho}t^{\prime}$.

  * •

r-beta. Then $t=(\lambda
x.\,s)\,\mathbf{v}\to_{\texttt{B}}s\\{x:=\mathbf{v}\\}=t^{\prime}$. The
conclusion of $\pi$ can then only be derived using rule t-app, so $\pi$ has
the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.44878pt\hbox{$\displaystyle\penalty
1\pi_{1}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}_{1}}s:\mathcal{T}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=100.67267pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\lambda
x.\,s:[\mathcal{S}^{?}\to\mathcal{T}]^{\mathsf{abs}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\end{array}(1)\ \mathcal{S}^{?}\lhd\mathcal{S}\hskip
14.22636pt\pi_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{v}:\mathcal{S}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=288.15718pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
72.03276pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}(\lambda
x.\,s)\,\mathbf{v}:\mathcal{T}$}}}}\end{array}$

where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$. Given (1), we
can apply Section 0.3.2 to $\pi_{1}$ with $\pi_{2}$, yielding
$\pi^{\prime}\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{\mathfrak{m}_{1}+\mathfrak{m}_{2}}s\\{x:=\mathbf{v}\\}:\mathcal{T}$,
and we conclude with
$\mathfrak{m}^{\prime}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$, since
$[\texttt{B}]+\mathfrak{m}^{\prime}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}=\mathfrak{m}$.

  * •

r-if0. Then $t=\mathsf{if}({\bf 0},s,x.\,u)\to_{\texttt{I0}}s=t^{\prime}$. The
conclusion of $\pi$ can then only be derived using rule t-ifZero, so $\pi$ has
the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
26.31105pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=56.97766pt\hbox{\kern
3.00003pt$\texttt{{t-zero}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\mathbb{0}]^{\mathsf{nat}}$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\end{array}\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}s:\mathcal{T}\par$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=193.28189pt\hbox{\kern
3.00003pt$\texttt{{t-ifZero}}$}}}\hbox{\kern
43.06238pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{[\texttt{I0}]+\mathfrak{m}^{\prime}}\mathsf{if}({\bf
0},s,x.\,u):\mathcal{T}$}}}}\end{array}$

where $\mathfrak{m}=[\texttt{I0}]+\mathfrak{m}^{\prime}$. It suffices to note
that $\pi^{\prime}$ is the needed derivation, so we are done.

  * •

r-ifS. Then
$t=\mathsf{if}(\mathbf{S}(\mathbf{k}),s,x.\,u)\to_{\texttt{IS}}u\\{x:=\mathbf{k}\\}=t^{\prime}$.
The conclusion of $\pi$ can then only be derived using rule t-ifSucc, so $\pi$
has the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
13.6832pt\hbox{$\displaystyle\penalty
1\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\mathbf{k}:\mathcal{N}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=97.3167pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}\mathbf{S}(\mathbf{k}):[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}\mathcal{N}^{?}\lhd\mathcal{N}\hskip
14.22636pt\pi_{2}\rhd\Phi_{2};\Gamma_{2},x:\mathcal{N}^{?}\vdash^{\mathfrak{m}_{2}}u:\mathcal{T}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=305.55193pt\hbox{\kern
3.00003pt$\texttt{{t-ifSucc}}$}}}\hbox{\kern
65.61787pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{IS}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}\mathsf{if}(\mathbf{S}(\mathbf{k}),s,x.\,u):\mathcal{T}$}}}}\end{array}$

where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\texttt{IS}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$. Applying
Section 0.3.2 on $\pi_{2}$ with $\pi_{1}$ leads us to
$\pi^{\prime}\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{\mathfrak{m}_{1}+\mathfrak{m}_{2}}u\\{x:=\mathbf{k}\\}:\mathcal{T}$,
where $\mathfrak{m}^{\prime}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and we
conclude since $[\texttt{IS}]+\mathfrak{m}^{\prime}=\mathfrak{m}$.

  * •

t-fix. Then
$t=\mathsf{fix}\,x.\,s\to_{\rho}s\\{x:=\mathsf{fix}\,x.\,s\\}=t^{\prime}$. The
conclusion of $\pi$ can then only be derived by rule t-fix, so $\pi$ has the
form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\pi_{0}\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}_{0}}s:\mathcal{T}\hskip
14.22636pt(\pi_{i}\rhd\Phi_{i};\Gamma_{i}\vdash^{\mathfrak{m}_{i}}\mathsf{fix}\,x.\,s:\mathcal{S}_{i})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=241.14198pt\hbox{\kern
3.00003pt$\texttt{{t-fix}}$}}}\hbox{\kern
43.51196pt\hbox{$\displaystyle\Phi_{0}+_{i\in I}\Phi_{i};\Gamma_{0}+_{i\in
I}\Gamma_{i}\vdash^{[\texttt{F}]+\mathfrak{m}_{0}+_{i\in
I}\mathfrak{m}_{i}}\mathsf{fix}\,x.\,s:\mathcal{T}$}}}}\end{array}$

where $\Phi=\Phi_{0}+_{i\in I}\Phi_{i}$ and $\Gamma=\Gamma_{0}+_{i\in
I}\Gamma_{i}$ and $\mathfrak{m}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{m}_{i}$.
By Section 0.3.2 on $\pi_{0}$ with $(\pi_{i})_{i\in I}$ we obtain
$\pi^{\prime}\rhd\Phi_{0}+_{i\in I}\Phi_{i};\Gamma_{0}+_{i\in
I}\Gamma_{i}\vdash^{\mathfrak{m}_{0}+_{i\in
I}\mathfrak{m}_{i}}s\\{x:=\mathsf{fix}\,x.\,s\\}:\mathcal{T}$. We let
$\mathfrak{m}^{\prime}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{m}_{i}$ and we
conclude since
$[\texttt{F}]+\mathfrak{m}^{\prime}=[\texttt{F}]+\mathfrak{m}_{0}+_{i\in
I}\mathfrak{m}_{i}=\mathfrak{m}$.

  * •

r-appL. Then $t=s\,u\to_{\rho}s^{\prime}\,u=t^{\prime}$, derived from
$s\to_{\rho}s^{\prime}$. The conclusion of $\pi$ can then only be derived by
rule t-app, so $\pi$ has the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathcal{S}^{?}\to\mathcal{T}]^{\mathsf{abs}}\hskip
14.22636pt(1)\ \mathcal{S}^{?}\lhd\mathcal{S}\hskip
14.22636pt\pi_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}u:\mathcal{S}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=240.50752pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
59.31442pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}s\,u:\mathcal{T}$}}}}\end{array}$

where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$. By the IH on
$s\to_{\rho}s^{\prime}$ and using $\pi_{1}$, there exists
$\mathfrak{m}^{\prime}_{1}$ such that
$\mathfrak{m}_{1}=[\rho]+\mathfrak{m}^{\prime}_{1}$ and
$\pi^{\prime}_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}^{\prime}_{1}}s^{\prime}:[\mathcal{S}^{?}\to\mathcal{T}]^{\mathsf{abs}}$.
Applying rule t-app with $\pi^{\prime}_{1}$, (1) and $\pi_{2}$ as premises, we
conclude with
$\pi^{\prime}\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{B}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}_{2}}s^{\prime}\,u:\mathcal{T}$.
We let
$\mathfrak{m}^{\prime}=[\texttt{B}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}_{2}$,
thus
$[\rho]+\mathfrak{m}^{\prime}=[\texttt{B}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}_{2}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}=\mathfrak{m}$.

  * •

r-appR. Analogous to the previous case.

  * •

r-succ. Then $t=\mathbf{S}(s)\to_{\rho}\mathbf{S}(s^{\prime})=t^{\prime}$,
derived from $s\to_{\rho}s^{\prime}$. The conclusion of $\pi$ can then only be
derived by rule t-succ, so $\pi$ has the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 4.12358pt\hbox{$\displaystyle\penalty
1\pi_{0}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}s:+_{i\in
I}\mathcal{M}_{i}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=95.90002pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(s):[\mathbb{S}(\mathcal{M}_{i})]^{\mathsf{nat}}_{i\in
I}$}}}}\end{array}$

where $\mathcal{T}=[\mathbb{S}(\mathcal{M}_{i})]^{\mathsf{nat}}_{i\in I}$. By
the IH on $s\to_{\rho}s^{\prime}$ and using $\pi_{0}$, there exists
$\mathfrak{m}^{\prime}$ such that $\mathfrak{m}=[\rho]+\mathfrak{m}^{\prime}$
and
$\pi^{\prime}_{0}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}s^{\prime}:+_{i\in
I}\mathcal{M}_{i}$. Applying rule t-succ with $\pi^{\prime}_{0}$ as premise,
we conclude with
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}\mathbf{S}(s^{\prime}):[\mathbb{S}(\mathcal{M}_{i})]^{\mathsf{nat}}_{i\in
I}$, where $\mathfrak{m}=[\rho]+\mathfrak{m}^{\prime}$.

  * •

r-if. Then
$t=\mathsf{if}(s,u,x.\,r)\to_{\rho}\mathsf{if}(s^{\prime},u,x.\,r)=t^{\prime}$,
derived from $s\to_{\rho}s^{\prime}$. The conclusion of $\pi$ can be derived
either by rule t-ifZero or by rule t-ifSucc. Let us suppose the first case, as
the second one is analogous. Then $\pi$ is of the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathbb{0}]^{\mathsf{nat}}\hskip
14.22636pt\pi_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}u:\mathcal{T}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=173.18326pt\hbox{\kern
3.00003pt$\texttt{{t-ifZero}}$}}}\hbox{\kern
6.50002pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{I0}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}}\mathsf{if}(s,u,x.\,r):\mathcal{T}$}}}}\end{array}$

where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\texttt{I0}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}$. By the IH on
$s\to_{\rho}s^{\prime}$ and using $\pi_{1}$, there exists
$\mathfrak{m}^{\prime}_{1}$ such that
$\mathfrak{m}_{1}=[\rho]+\mathfrak{m}^{\prime}_{1}$ and
$\pi^{\prime}_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}^{\prime}_{1}}s^{\prime}:[\mathbb{0}]^{\mathsf{nat}}$.
Applying rule t-ifZero with $\pi^{\prime}_{1}$ and $\pi_{2}$ as premises, we
conclude with
$\pi^{\prime}\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{I0}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}_{2}}\mathsf{if}(s^{\prime},u,x.\,r):\mathcal{T}$.
We let
$\mathfrak{m}^{\prime}=[\texttt{I0}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}_{2}$,
thus
$[\rho]+\mathfrak{m}^{\prime}=[\rho]+[\texttt{I0}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}_{2}=[\texttt{I0}]+\mathfrak{m}_{1}+\mathfrak{m}_{2}=\mathfrak{m}$.

∎

*

###### Proof.

We first consider the case $t=x$, for which we have
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{v}:\mathcal{T}$ as
hypothesis. Then taking $\Phi_{1}:=\varnothing$ and $\Phi_{2}:=\Phi$ and
$\Gamma_{1}:=\varnothing$ and $\Gamma_{2}:=\Gamma$ and
$\mathfrak{m}_{1}:=[\,]$ and $\mathfrak{m}_{2}:=\mathfrak{m}$ and
$\mathcal{S}^{?}:=\mathcal{T}$ and $\mathcal{S}:=\mathcal{T}$, we conclude
that the following hold:

  1. 1.

$\pi\rhd\varnothing;x:\mathcal{T}\vdash^{[\,]}x:\mathcal{T}$, by rule t-var1

  2. 2.

$\zeta\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{v}:\mathcal{T}$, by letting
$\zeta:=\pi^{\prime}$

  3. 3.

$\Phi=\varnothing+\Phi=\Phi_{1}+\Phi_{2}$ and
$\Gamma=\varnothing+\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\,]+\mathfrak{m}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$\mathcal{T}\lhd\mathcal{T}$

If $t\neq x$, then we proceed by induction on $\pi^{\prime}$.

  * •

t-var1. Then $t=y$, with $y\neq x$, and
$\pi^{\prime}\rhd\varnothing;y:\mathcal{T}\vdash^{[\,]}y:\mathcal{T}$, where
$\Phi=\varnothing$ and $\Gamma=y:\mathcal{T}$ and $\mathfrak{m}=[\,]$. Taking
$\Phi_{1}=\Phi_{2}:=\varnothing$ and $\Gamma_{1}:=y:\mathcal{T}$ and
$\Gamma_{2}:=\varnothing$ and $\mathfrak{m}_{1}=\mathfrak{m}_{2}:=[\,]$ and
$\mathcal{S}^{?}:=\bot$ and $\mathcal{S}:=[\,]^{\nu}$ with $\nu$ a proper
nature, we conclude with:

    1. 1.

$\pi\rhd\varnothing;y:\mathcal{T},x:\bot\vdash^{[\,]}y:\mathcal{T}$, by
letting $\pi:=\pi^{\prime}$

    2. 2.

$\zeta\rhd\varnothing;\varnothing\vdash^{[\,]}\mathbf{v}:[\,]^{\nu}$, by Lemma
3

    3. 3.

$\Phi=\varnothing=\varnothing+\varnothing=\Phi_{1}+\Phi_{2}$ and
$\Gamma=(y:\mathcal{T})+\varnothing=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=[\,]=[\,]+[\,]=\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$\bot\lhd[\,]^{\nu}$.

  * •

t-var2. Analogous to the previous case.

  * •

t-abs. Then $\pi^{\prime}\rhd+_{i\in I}\Phi_{i};+_{i\in
I}\Gamma_{i}\vdash^{+_{i\in I}\mathfrak{m}_{i}}\lambda
y.\,s:[\mathcal{U}^{?}_{i}\to\mathcal{R}_{i}]^{\mathsf{abs}}_{i\in I}$, with
$\Phi=+_{i\in I}\Phi_{i}$ and $\Gamma=+_{i\in I}\Gamma_{i}$ and
$\mathfrak{m}=+_{i\in I}\mathfrak{m}_{i}$ and
$\mathcal{T}=[\mathcal{U}^{?}_{i}\to\mathcal{R}_{i}]^{\mathsf{abs}}_{i\in I}$.
Then $t=\lambda y.\,s^{\prime}$, with $s=s^{\prime}\\{x:=\mathbf{v}\\}$. The
judgment is derived from premises of the form
$\pi^{\prime}_{i}\rhd\Phi_{i};\Gamma_{i},y:\mathcal{U}^{?}_{i}\vdash^{\mathfrak{m}_{i}}s:\mathcal{R}_{i}$
for each ${i\in I}$. We can apply the IH on $(\pi_{i})_{i\in I}$, yielding
that for each ${i\in I}$ there exist family contexts $\Phi_{i1}$, $\Phi_{i2}$,
typing contexts $\Gamma_{i1}$, $\Gamma_{i2}$, multi-counters
$\mathfrak{m}_{i1}$, $\mathfrak{m}_{i2}$, an optional multitype
$\mathcal{S}^{?}_{i}$ and a multitype $\mathcal{S}_{i}$ such that:

    1. i.1.

$(\pi_{i}\rhd\Phi_{i1};\Gamma_{i1},y:\mathcal{U}^{?}_{i},x:\mathcal{S}^{?}_{i}\vdash^{\mathfrak{m}_{i1}}s^{\prime}:\mathcal{R}_{i})_{i\in
I}$

    2. i.2.

$(\zeta_{i}\rhd\Phi_{i2};\Gamma_{i2}\vdash^{\mathfrak{m}_{i2}}\mathbf{v}:\mathcal{S}_{i})_{i\in
I}$

    3. i.3.

$\Phi_{i}=\Phi_{i1}+\Phi_{i2}$ and
$\Gamma_{i},y:\mathcal{U}^{?}_{i}=(\Gamma_{i1},y:\mathcal{U}^{?}_{i})+\Gamma_{i2}$
and $\mathfrak{m}_{i}=\mathfrak{m}_{i1}+\mathfrak{m}_{i2}$ and
$\mathcal{S}^{?}_{i}\lhd\mathcal{S}_{i}$.

For each ${i\in I}$, it is not necessary to split $y:\mathcal{U}^{?}_{i}$, as
we may assume $y\notin\mathsf{fv}(\mathbf{v})$ by $\alpha$-conversion, so
$x\notin\mathsf{dom}(\Gamma_{i2})$ by Lemma 2. Taking $\Phi_{1}:=+_{i\in
I}\Phi_{i1}$ and $\Phi_{2}:=+_{i\in I}\Phi_{i2}$ and $\Gamma_{1}:=+_{i\in
I}\Gamma_{i1}$ and $\Gamma_{2}:=+_{i\in I}\Gamma_{i2}$ and
$\mathfrak{m}_{1}:=+_{i\in I}\mathfrak{m}_{i1}$ and $\mathfrak{m}_{2}:=+_{i\in
I}\mathfrak{m}_{i2}$ and $\mathcal{S}^{?}:=+_{i\in I}\mathcal{S}^{?}_{i}$ and
$\mathcal{S}:=+_{i\in I}\mathcal{S}_{i}$ we conclude with:

    1. 1.

$\pi\rhd+_{i\in I}\Phi_{i1};+_{i\in I}\Gamma_{i1},x:+_{i\in
I}\mathcal{S}_{i}\vdash^{+_{i\in I}\mathfrak{m}_{i1}}\lambda
y.\,s^{\prime}:[\mathcal{U}^{?}_{i}\to\mathcal{R}_{i}]^{\mathsf{abs}}_{i\in
I}$, by applying rule t-abs to $(\pi_{i})_{i\in I}$

    2. 2.

$\zeta\rhd+_{i\in I}\Phi_{i2};+_{i\in I}\Gamma_{i2}\vdash^{+_{i\in
I}\mathfrak{m}_{i2}}\mathbf{v}:+_{i\in I}\mathcal{S}_{i}$, as the result of
applying Lemma 4 to $(\zeta_{i})_{i\in I}$

    3. 3.

$\Phi=+_{i\in I}\Phi_{i}=+_{i\in I}(\Phi_{i1}+\Phi_{i2})=\Phi_{1}+\Phi_{2}$
and $\Gamma=+_{i\in I}\Gamma_{i}=+_{i\in
I}(\Gamma_{i1}+\Gamma_{i2})=\Gamma_{1}+\Gamma_{2}$ and $\mathfrak{m}=+_{i\in
I}\mathfrak{m}_{i}=+_{i\in
I}(\mathfrak{m}_{i1}+\mathfrak{m}_{i2})=\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$+_{i\in I}\mathcal{S}^{?}_{i}\lhd+_{i\in I}\mathcal{S}_{i}$ by Lemma 4

  * •

t-app. Then
$\pi^{\prime}\rhd\Phi_{a}+\Phi_{b};\Gamma_{a}+\Gamma_{b}\vdash^{[\texttt{B}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}}s\,u:\mathcal{T}$,
where $\Phi=\Phi_{a}+\Phi_{b}$ and $\Gamma=\Gamma_{a}+\Gamma_{b}$ and
$\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}$. Since $t\neq
x$, then $t=s^{\prime}\,u^{\prime}$ with $s=s^{\prime}\\{x:=\mathbf{v}\\}$ and
$u=u^{\prime}\\{x:=\mathbf{v}\\}$. The judgment is derived from
$\pi^{\prime}_{a}\rhd\Phi_{a};\Gamma_{a}\vdash^{\mathfrak{m}_{a}}s:[\mathcal{U}^{?}\to\mathcal{T}]^{\mathsf{abs}}$
and
$\pi^{\prime}_{b}\rhd\Phi_{b};\Gamma_{b}\vdash^{\mathfrak{m}_{b}}u:\mathcal{U}$,
where $\mathcal{U}^{?}\lhd\mathcal{U}$. We can apply IH on $\pi_{a}$, yielding
that there exist family contexts $\Phi_{a1}$, $\Phi_{a2}$, typing contexts
$\Gamma_{a1}$, $\Gamma_{a2}$, multi-counters $\mathfrak{m}_{a1}$,
$\mathfrak{m}_{a2}$, an optional multitype $\mathcal{S}^{?}_{a}$ and a
multitype $\mathcal{S}_{a}$ satisfying:

    1. a.1.

$\pi_{a}\rhd\Phi_{a1};\Gamma_{a1},x:\mathcal{S}^{?}_{a}\vdash^{\mathfrak{m}_{a1}}s^{\prime}:[\mathcal{U}^{?}\to\mathcal{T}]^{\mathsf{abs}}$

    2. a.2.

$\zeta_{a}\rhd\Phi_{a2};\Gamma_{a2}\vdash^{\mathfrak{m}_{a2}}\mathbf{v}:\mathcal{S}_{a}$

    3. a.3.

$\Phi_{a}=\Phi_{a1}+\Phi_{a2}$ and $\Gamma_{a}=\Gamma_{a1}+\Gamma_{a2}$ and
$\mathfrak{m}_{1}=\mathfrak{m}_{a1}+\mathfrak{m}_{a2}$ and
$\mathcal{S}^{?}_{a}\lhd\mathcal{S}_{a}$

On the other hand we can apply IH on $\pi_{b}$, yielding that there exist
family contexts $\Phi_{b1}$, $\Phi_{b2}$, typing contexts $\Gamma_{b1}$,
$\Gamma_{b2}$, multi-counters $\mathfrak{m}_{b1}$, $\mathfrak{m}_{b2}$, an
optional multitype $\mathcal{S}^{?}_{b}$ and a multitype $\mathcal{S}_{b}$
satisfying:

    1. b.1.

$\pi_{b}\rhd\Phi_{b1};\Gamma_{b1},x:\mathcal{S}^{?}_{b}\vdash^{\mathfrak{m}_{b1}}u^{\prime}:\mathcal{U}$

    2. b.2.

$\zeta_{b}\rhd\Phi_{b2};\Gamma_{b2}\vdash^{\mathfrak{m}_{b2}}\mathbf{v}:\mathcal{S}_{b}$

    3. b.3.

$\Phi_{b}=\Phi_{b1}+\Phi_{b2}$ and $\Gamma_{b}=\Gamma_{b1}+\Gamma_{b2}$ and
$\mathfrak{m}_{b}=\mathfrak{m}_{b1}+\mathfrak{m}_{b2}$ and
$\mathcal{S}^{?}_{b}\lhd\mathcal{S}_{b}$

Then, taking $\Phi_{1}:=\Phi_{a1}+\Phi_{b1}$ and
$\Phi_{2}:=\Phi_{a2}+\Phi_{b2}$ and $\Gamma_{1}:=\Gamma_{a1}+\Gamma_{b1}$ and
$\Gamma_{2}:=\Gamma_{a2}+\Gamma_{b2}$ and
$\mathfrak{m}_{1}:=[\texttt{B}]+\mathfrak{m}_{a1}+\mathfrak{m}_{b1}$ and
$\mathfrak{m}_{2}:=\mathfrak{m}_{a2}+\mathfrak{m}_{b2}$ and
$\mathcal{S}^{?}:=\mathcal{S}^{?}_{a}+\mathcal{S}^{?}_{b}$ and
$\mathcal{S}:=\mathcal{S}_{a}+\mathcal{S}_{b}$, we conclude that the following
hold:

    1. 1.

$\pi\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}_{1}}s^{\prime}\,u^{\prime}:\mathcal{T}$,
by applying rule t-app with $\pi_{a}$ and $\pi_{b}$ as premises, given that
$\mathcal{U}^{?}\lhd\mathcal{U}$ holds

    2. 2.

$\zeta\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{v}:\mathcal{S}$,
as the result of applying Lemma 7 to $\zeta_{a}$ and $\zeta_{b}$

    3. 3.

It is easy to check that the remaining conditions hold.

  * •

t-zero. Analogous to case t-var1.

  * •

t-succ. Then
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(u):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$, where $\mathcal{T}=[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$. Since $t\neq x$, then $t=\mathbf{S}(u^{\prime})$, with
$u=u^{\prime}\\{x:=\mathbf{v}\\}$. The judgment is derived from
$\pi^{\prime}_{0}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}u:\mathcal{N}$, where
$\mathcal{N}=+_{i\in I}\mathcal{N}_{i}$. We can apply IH on
$\pi^{\prime}_{0}$, yielding that there exist family contexts $\Phi_{1}$,
$\Phi_{2}$, typing contexts $\Gamma_{1}$, $\Gamma_{2}$, multi-counters
$\mathfrak{m}_{1}$, $\mathfrak{m}_{2}$, an optional multitype
$\mathcal{S}^{?}$ and a multitype $\mathcal{S}$ such that:

    1. 1’.

$\pi_{0}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}_{1}}u^{\prime}:\mathcal{N}$,
where $\mathcal{N}=+_{i\in I}\mathcal{N}_{i}$

    2. 2’.

$\zeta_{0}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{v}:\mathcal{S}$

    3. 3’.

$\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$ and
$\mathcal{S}^{?}\lhd\mathcal{S}$

By taking $\Phi_{1}$, $\Phi_{2}$, $\Gamma_{1}$, $\Gamma_{2}$,
$\mathfrak{m}_{1}$, $\mathfrak{m}_{2}$, $\mathcal{S}^{?}$ and $\mathcal{S}$
from the IH, we conclude that
$\pi\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}_{1}}\mathbf{S}(u^{\prime}):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$, by applying rule t-succ to $\pi_{0}$. The remaining conditions to met
already hold by the IH, letting $\zeta:=\zeta_{0}$.

  * •

t-ifZero. Analogous to case t-app.

  * •

t-ifSucc. Then
$\pi^{\prime}\rhd\Phi_{a}+\Phi_{b};\Gamma_{a}+\Gamma_{b}\vdash^{[\texttt{IS}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}}\mathsf{if}(s,u,y.\,r):\mathcal{T}$,
where $\Phi=\Phi_{a}+\Phi_{b}$ and $\Gamma=\Gamma_{a}+\Gamma_{b}$ and
$\mathfrak{m}=[\texttt{IS}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}$. Then
$t=\mathsf{if}(s^{\prime},u^{\prime},y.\,r^{\prime})$, where
$s=s^{\prime}\\{x:=\mathbf{v}\\}$, $u=u^{\prime}\\{x:=\mathbf{v}\\}$ and
$r=r^{\prime}\\{x:=\mathbf{v}\\}$. The judgment is derived from
$\pi^{\prime}_{a}\rhd\Phi_{a};\Gamma_{a}\vdash^{\mathfrak{m}_{a}}s:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$
and
$\pi^{\prime}_{b}\rhd\Phi_{b};\Gamma_{b},y:\mathcal{N}^{?}\vdash^{\mathfrak{m}_{b}}r:\mathcal{T}$,
with $\mathcal{N}^{?}\lhd\mathcal{N}$. We can apply IH on $\pi^{\prime}_{a}$,
yielding that there exist family contexts $\Phi_{a1}$, $\Phi_{a2}$, typing
contexts $\Gamma_{a1}$, $\Gamma_{a2}$, multi-counters $\mathfrak{m}_{a1}$,
$\mathfrak{m}_{a2}$, an optional multitype $\mathcal{S}^{?}_{a}$ and a
multitype $\mathcal{S}_{a}$ such that:

    1. a.1.

$\pi_{a}\rhd\Phi_{a1};\Gamma_{a1},x:\mathcal{S}^{?}_{a}\vdash^{\mathfrak{m}_{a1}}s^{\prime}:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$

    2. a.2.

$\zeta_{a}\rhd\Phi_{a2};\Gamma_{a2}\vdash^{\mathfrak{m}_{a2}}\mathbf{v}:\mathcal{S}_{a}$

    3. a.3.

$\Phi_{a}=\Phi_{a1}+\Phi_{a2}$ and $\Gamma_{a}=\Gamma_{a1}+\Gamma_{a2}$ and
$\mathfrak{m}_{a}=\mathfrak{m}_{a1}+\mathfrak{m}_{a2}$ and
$\mathcal{S}^{?}_{a}\lhd\mathcal{S}_{a}$

And we can apply the IH on $\pi^{\prime}_{b}$, yielding that there exist
family contexts $\Phi_{b1}$, $\Phi_{b2}$, typing contexts $\Gamma_{b1}$,
$\Gamma_{b2}$, multi-counters $\mathfrak{m}_{b1}$, $\mathfrak{m}_{b2}$, an
optional multitype $\mathcal{S}^{?}_{b}$ and a multitype $\mathcal{S}_{b}$
such that:

    1. b.1.

$\pi_{b}\rhd\Phi_{b1};\Gamma_{b1},y:\mathcal{N}^{?},x:\mathcal{S}^{?}_{b}\vdash^{\mathfrak{m}_{b1}}r^{\prime}:\mathcal{T}$

    2. b.2.

$\zeta_{b}\rhd\Phi_{b2};\Gamma_{b2}\vdash^{\mathfrak{m}_{b2}}\mathbf{v}:\mathcal{S}_{b}$

    3. b.3.

$\Phi_{b}=\Phi_{b1}+\Phi_{b2}$ and $\Gamma_{b}=\Gamma_{b1}+\Gamma_{b2}$ and
$\mathfrak{m}_{b}=\mathfrak{m}_{b1}+\mathfrak{m}_{b2}$ and
$\mathcal{S}^{?}_{b}\lhd\mathcal{S}_{b}$.

We are allowed to split $\Gamma_{b},y:\mathcal{N}^{?}$ into
$(\Gamma_{b1},y:\mathcal{N}^{?})$ and $\Gamma_{b2}$ by Lemma 2, since by
$\alpha$-conversion we can assume $y\notin\mathsf{fv}(\mathbf{v})$. Taking
$\Phi_{1}:=\Phi_{a1}+\Phi_{b1}$ and $\Phi_{2}:=\Phi_{a2}+\Phi_{b2}$ and
$\Gamma_{1}:=\Gamma_{a1}+\Gamma_{b1}$ and
$\Gamma_{2}:=\Gamma_{a2}+\Gamma_{b2}$ and
$\mathfrak{m}_{1}:=[\texttt{IS}]+\mathfrak{m}_{a1}+\mathfrak{m}_{b1}$ and
$\mathfrak{m}_{2}:=\mathfrak{m}_{a2}+\mathfrak{m}_{b2}$ and
$\mathcal{S}^{?}:=\mathcal{S}^{?}_{a}+\mathcal{S}^{?}_{b}$ and
$\mathcal{S}:=\mathcal{S}_{a}+\mathcal{S}_{b}$, we conclude that the following
hold:

    1. 1.

$\pi\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}_{1}}\mathsf{if}(s^{\prime},y,u^{\prime}.\,r^{\prime}):\mathcal{T}$,
by applying rule t-ifSucc to $\pi_{a}$ and $\pi_{b}$, given that
$\mathcal{N}^{?}\lhd\mathcal{N}$ holds

    2. 2.

$\zeta\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{v}:\mathcal{S}$,
as the result of applying Lemma 7 to $\zeta_{a}$ and $\zeta_{b}$

    3. 3.

$\mathfrak{m}=[\texttt{IS}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}=\mathfrak{m}_{1}+\mathfrak{m}_{2}$,
and it is easy to check that the remaining conditions hold

  * •

t-fix. Then $\pi^{\prime}\rhd\Phi_{0}+_{i\in I}\Phi_{i};\Gamma_{0}+_{i\in
I}\Gamma_{i}\vdash^{[\texttt{F}]+\mathfrak{m}_{0}+_{i\in
I}\mathfrak{m}_{i}}\mathsf{fix}\,y.\,s:\mathcal{T}$, where
$\Phi=\Phi_{0}+_{i\in I}\Phi_{i}$ and $\Gamma=\Gamma_{0}+_{i\in I}\Gamma_{i}$
and $\mathfrak{m}=[\texttt{F}]+\mathfrak{m}_{0}+_{i\in I}\mathfrak{m}_{i}$.
Then $t=\mathsf{fix}\,y.\,s^{\prime}$, where
$s=s^{\prime}\\{x:=\mathbf{v}\\}$. The judgment is derived from
$\pi^{\prime}_{0}\rhd\Phi_{0},y:\\{\\!\\!\\{\mathcal{U}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}_{0}}s:\mathcal{T}$ and
$(\pi^{\prime}_{i}\rhd\Phi_{i};\Gamma_{i}\vdash^{\mathfrak{m}_{i}}\mathsf{fix}\,y.\,s:\mathcal{U}_{i})_{i\in
I}$. We can then apply the IH on $\pi^{\prime}_{0}$, yielding that then there
exist family contexts $\Phi_{01}$, $\Phi_{02}$, typing contexts $\Gamma_{01}$,
$\Gamma_{02}$, multi-counters $\mathfrak{m}_{01}$, $\mathfrak{m}_{02}$, an
optional multitype $\mathcal{S}^{?}_{0}$ and a multitype $\mathcal{S}_{0}$
such that:

    1. 1’.

$\pi_{0}\rhd\Phi_{01},y:\\{\\!\\!\\{\mathcal{U}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{01},x:\mathcal{S}^{?}_{0}\vdash^{\mathfrak{m}_{01}}s^{\prime}:\mathcal{T}$

    2. 2’.

$\zeta_{0}\rhd\Phi_{02};\Gamma_{02}\vdash^{\mathfrak{m}_{02}}\mathbf{v}:\mathcal{S}_{0}$

    3. 3’.

$\Phi_{0}=\Phi_{01}+\Phi_{02}$ and $\Gamma_{0}=\Gamma_{01}+\Gamma_{02}$ and
$\mathfrak{m}_{0}=\mathfrak{m}_{01}+\mathfrak{m}_{02}$ and
$\mathcal{S}^{?}_{0}\lhd\mathcal{S}_{0}$.

Note that it is not necessary to split
$\\{\\!\\!\\{\mathcal{U}_{i}\\}\\!\\!\\}_{i\in I}$ since we may assume
$y\notin\mathsf{fv}(\mathbf{v})$ by $\alpha$-conversion, so
$y\notin\mathsf{dom}(\Phi_{02})$ by Lemma 2. The conclusions of
$\pi^{\prime}_{i}$ for each ${i\in I}$ are smaller than $\pi^{\prime}$, hence
we can apply the IH on $(\pi^{\prime}_{i})_{i\in I}$, yielding that for each
${i\in I}$ there exist family contexts $(\Phi_{i1})_{i\in I}$,
$(\Phi_{i2})_{i\in I}$, typing contexts $(\Gamma_{i1})_{i\in I}$,
$(\Gamma_{i2})_{i\in I}$, multi-counters $(\mathfrak{m}_{i1})_{i\in I}$,
$(\mathfrak{m}_{i2})_{i\in I}$, an optional multitype
$(\mathcal{S}^{?}_{i})_{i\in I}$ and a multitype $(\mathcal{S}_{i})_{i\in I}$
such that:

    1. i.1.

$\pi_{i}\rhd\Phi_{i1};\Gamma_{i1},x:\mathcal{S}^{?}_{i}\vdash^{\mathfrak{m}_{i1}}\mathsf{fix}\,y.\,s^{\prime}:\mathcal{U}_{i}$

    2. i.2.

$\zeta_{i}\rhd\Phi_{i2};\Gamma_{i2}\vdash^{\mathfrak{m}_{i2}}\mathbf{v}:\mathcal{S}_{i}$

    3. i.3.

$\Phi_{i}=\Phi_{i1}+\Phi_{i2}$ and $\Gamma_{i}=\Gamma_{i1}+\Gamma_{i2}$ and
$\mathfrak{m}_{i}=\mathfrak{m}_{i1}+\mathfrak{m}_{i2}$ and
$\mathcal{S}^{?}_{i}\lhd\mathcal{S}_{i}$

Taking $\Phi_{1}:=\Phi_{01}+_{i\in I}\Phi_{i1}$ and
$\Phi_{2}:=\Phi_{02}+_{i\in I}\Phi_{i2}$ and $\Gamma_{1}:=\Gamma_{01}+_{i\in
I}\Gamma_{i1}$ and $\Gamma_{2}:=\Gamma_{02}+_{i\in I}\Gamma_{i2}$ and
$\mathfrak{m}_{1}:=[\texttt{F}]+\mathfrak{m}_{01}+_{i\in I}\mathfrak{m}_{i1}$
and $\mathfrak{m}_{2}:=\mathfrak{m}_{02}+_{i\in I}\mathfrak{m}_{i2}$ and
$\mathcal{S}^{?}:=\mathcal{S}^{?}_{0}+_{i\in I}\mathcal{S}^{?}_{i}$, and
$\mathcal{S}:=\mathcal{S}_{0}+_{i\in I}\mathcal{S}_{i}$, we conclude that the
following hold:

    1. 1.

$\pi\rhd\
\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}_{1}}\mathsf{fix}\,y.\,s^{\prime}:\mathcal{T}$,
by applying rule t-fix to $\pi_{0}$ and $(\pi_{i})_{i\in I}$

    2. 2.

$\zeta\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}_{2}}\mathbf{v}:\mathcal{S}$,
as the result of applying Lemma 4 to $\zeta_{0}$ and $(\zeta_{i})_{i\in I}$

    3. 3.

It is easy to check that the remainder conditions hold.

∎

*

###### Proof.

We first consider the case $t=x$, for which we have
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}q:\mathcal{T}$ as hypothesis.
Taking a set $I$ such that its cardinality is 1, and $\Phi_{0}:=\varnothing$,
$\Psi:=\Phi$ and $\Gamma_{0}:=\varnothing$, $\Delta:=\Gamma$ and
$\mathfrak{m}_{0}:=[\,]$, $\mathfrak{n}:=\mathfrak{m}$ and
$\mathcal{S}:=\mathcal{T}$, then the following hold:

  1. 1.

$\pi\rhd
x:\\{\\!\\!\\{\mathcal{T}\\}\\!\\!\\};\varnothing\vdash^{[\,]}x:\mathcal{T}$,
by rule t-var2

  2. 2.

$\zeta_{i}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}q:\mathcal{T}$, by hypothesis,
since $I$ is a singleton, and we let $\zeta_{i}:=\pi^{\prime}$

  3. 3.

$\Phi=\varnothing+\Phi=\Phi_{0}+\Psi$ and
$\Gamma=\varnothing+\Gamma=\Gamma_{0}+\Delta$ and
$\mathfrak{m}=[\,]+\mathfrak{m}=\mathfrak{m}_{0}+\mathfrak{n}$

If $t\neq x$ then we proceed by induction on $\pi^{\prime}$.

  * •

t-var1. Then $t=y$, with $y\neq x$, and
$\pi^{\prime}\rhd\varnothing;y:\mathcal{T}\vdash^{[\,]}y:\mathcal{T}$, with
$\Phi=\varnothing$ and $\Gamma=y:\mathcal{T}$ and $\mathfrak{m}=[\,]$. Taking
$I:=\varnothing$ and $\Phi_{0}:=\Phi$ and $\Gamma_{0}:=\Gamma$ and
$\mathfrak{m}_{0}:=\mathfrak{m}$, we conclude with
$\pi\rhd\varnothing;y:\mathcal{T}\vdash^{[\,]}y:\mathcal{T}$ by letting
$\pi:=\pi^{\prime}$. Item 2 and Item 3 hold trivially since $I=\varnothing$.

  * •

t-var2. Analogous to the previous case.

  * •

t-abs. Then $\pi^{\prime}\rhd+_{j\in J}\Phi_{j};+_{j\in
J}\Gamma_{j}\vdash^{+_{j\in J}\mathfrak{m}_{j}}\lambda
y.\,s:[\mathcal{U}^{?}_{j}\to\mathcal{R}_{j}]^{\mathsf{abs}}_{j\in J}$, with
$\Phi=+_{j\in J}\Phi_{j}$ and $\Gamma=+_{j\in J}\Gamma_{j}$ and
$\mathfrak{m}=+_{j\in J}\mathfrak{m}_{j}$ and
$\mathcal{T}=[\mathcal{U}^{?}_{j}\to\mathcal{R}_{j}]^{\mathsf{abs}}_{j\in J}$.
Then $t=\lambda y.\,s^{\prime}$, with $s=s^{\prime}\\{x:=q\\}$. The judgment
is derived from premises of the form
$\pi^{\prime}_{j}\rhd\Phi_{j};\Gamma_{j},y:\mathcal{U}^{?}_{j}\vdash^{\mathfrak{m}_{j}}s:\mathcal{R}_{j}$
for each ${j\in J}$. We can apply the IH on $(\pi^{\prime}_{j})_{j\in J}$,
yielding that for each ${j\in J}$ there exist a finite set $I_{j}$, family
contexts $\Phi_{j0}$ and $(\Psi_{k})_{k\in I_{j}}$, typing contexts
$\Gamma_{j0}$ and $(\Delta_{k})_{k\in I_{j}}$, multi-counters and
$\mathfrak{m}_{j0}$ and $(\mathfrak{n}_{k})_{k\in I_{j}}$ and multitypes
$(\mathcal{S}_{k})_{k\in I_{j}}$ such that:

    1. j.1.

$\pi_{j}\rhd\Phi_{j0},x:\\{\\!\\!\\{\mathcal{S}_{k}\\}\\!\\!\\}_{k\in
I_{j}};\Gamma_{j0},y:\mathcal{U}^{?}_{j}\vdash^{\mathfrak{m}_{j0}}s^{\prime}:\mathcal{R}_{j}$

    2. j.2.

$(\zeta_{k}\rhd\Psi_{k};\Delta_{k}\vdash^{\mathfrak{n}_{k}}q:\mathcal{S}_{k})_{k\in
I_{j}}$

    3. j.3.

$\Phi_{j}=\Phi_{j0}+_{k\in I_{j}}\Psi_{k}$ and
$\Gamma_{j},y:\mathcal{U}^{?}_{j}=\Gamma_{j0},y:\mathcal{U}^{?}_{j}+_{k\in
I_{j}}\Delta_{k}$ and $\mathfrak{m}_{j}=\mathfrak{m}_{j0}+_{k\in
I_{j}}\mathfrak{n}_{k}$.

Note that for each ${j\in J}$ it is not necessary to split
$\mathcal{U}^{?}_{j}$ since we may assume $y\notin\mathsf{fv}(q)$ by
$\alpha$-conversion, so $y\notin\mathsf{dom}(+_{k\in I_{j}}\Delta_{k})$ by
Lemma 2. Taking $I:=\uplus_{j\in J}I_{j}$ and $\Phi_{0}:=+_{j\in J}\Phi_{j0}$
and $\Psi_{i}:=+_{k\in I_{j}}\Psi_{k}$ and $\Gamma_{0}:=+_{j\in J}\Gamma_{j0}$
and $\Delta_{i}:=+_{k\in I_{j}}\Delta_{k}$ and $\mathfrak{m}_{0}:=+_{j\in
J}\mathfrak{m}_{j0}$ and $\mathfrak{n}_{i}:=+_{k\in I_{j}}\mathfrak{n}_{k}$
and $\mathcal{S}_{i}:=+_{k\in I_{j}}\mathcal{S}_{k}$, we have:

    1. 1.

$\pi\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}_{0}}\lambda
y.\,s^{\prime}:[\mathcal{U}^{?}_{j}\to\mathcal{R}_{j}]^{\mathsf{abs}}_{j\in
J}$, by applying rule t-abs to $(\pi_{j})_{j\in J}$

    2. 2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I}$, as the result of applying Lemma 4 to $(\zeta_{k})_{k\in I_{j}}$ for each
${j\in J}$

    3. 3.

$\Phi=+_{j\in J}\Phi_{j}=+_{j\in J}(\Phi_{j0}+_{k\in
I_{j}}\Psi_{k})=\Phi_{0}+_{i\in I}\Psi_{i}$ and $\Gamma=+_{j\in
J}\Gamma_{j}=+_{j\in J}(\Gamma_{j0}+_{k\in I_{j}}\Delta_{k})=\Gamma_{0}+_{i\in
I}\Delta_{i}$ and $\mathfrak{m}=+_{j\in J}\mathfrak{m}_{j}=+_{j\in
J}(\mathfrak{m}_{j0}+_{k\in I_{j}}\mathfrak{n}_{k})=\mathfrak{m}_{0}+_{i\in
I}\mathfrak{n}_{i}$

  * •

t-app. Then
$\pi^{\prime}\rhd\Phi_{a}+\Phi_{b};\Gamma_{a}+\Gamma_{b}\vdash^{[\texttt{B}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}}s\,u:\mathcal{T}$,
with $\Phi=\Phi_{a}+\Phi_{b}$ and $\Gamma=\Gamma_{a}+\Gamma_{b}$ and
$\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}$. Then
$t=s^{\prime}\,u^{\prime}$, with $s\,u=(s^{\prime}\,u^{\prime})\\{x:=q\\}$.
The judgment is derived from
$\pi^{\prime}_{a}\rhd\Phi_{a};\Gamma_{a}\vdash^{\mathfrak{m}_{a}}s:[\mathcal{U}^{?}\to\mathcal{T}]^{\mathsf{abs}}$
and
$\pi^{\prime}_{b}\rhd\Phi_{b};\Gamma_{b}\vdash^{\mathfrak{m}_{b}}u:\mathcal{U}$,
where $\mathcal{U}^{?}\lhd\mathcal{U}$. We can apply the IH on $\pi_{a}$,
yielding that there exist a finite set $I_{a}$, family contexts $\Phi_{a0}$
and $(\Psi_{i})_{i\in I_{a}}$, typing contexts $\Gamma_{a0}$ and
$(\Delta_{i})_{i\in I_{a}}$, multi-counters $\mathfrak{m}_{a0}$ and
$(\mathfrak{n}_{i})_{i\in I_{a}}$ and multitypes $(\mathcal{S}_{i})_{i\in
I_{a}}$ such that:

    1. a.1.

$\pi_{a}\rhd\Phi_{a0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I_{a}};\Gamma_{a0}\vdash^{\mathfrak{m}_{a0}}s^{\prime}:[\mathcal{U}^{?}\to\mathcal{T}]^{\mathsf{abs}}$

    2. a.2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I_{a}}$

    3. a.3.

$\Phi_{a}=\Phi_{a0}+_{i\in I_{a}}\Psi_{i}$ and $\Gamma_{a}=\Gamma_{a0}+_{i\in
I_{a}}\Delta_{i}$ and $\mathfrak{m}_{a}=\mathfrak{m}_{a0}+_{i\in
I_{a}}\mathfrak{n}_{i}$

And we can apply the IH on $\pi_{b}$, yielding that there exist a finite set
$I_{b}$, family contexts $\Phi_{b0}$ and $(\Psi_{i})_{i\in I_{b}}$, typing
contexts $\Gamma_{b0}$ and $(\Delta_{i})_{i\in I_{b}}$, multi-counters
$\mathfrak{m}_{b0}$ and $(\mathfrak{n}_{i})_{i\in I_{b}}$ and multitypes
$(\mathcal{S}_{i})_{i\in I_{b}}$ such that:

    1. b.1.

$\pi_{b}\rhd\Phi_{b0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I_{b}};\Gamma_{b0}\vdash^{\mathfrak{m}_{b0}}u^{\prime}:\mathcal{U}$

    2. b.2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I_{b}}$

    3. b.3.

$\Phi_{b}=\Phi_{b0}+_{i\in I_{b}}\Psi_{i}$ and $\Gamma_{b}=\Gamma_{b0}+_{i\in
I_{b}}\Delta_{i}$ and $\mathfrak{m}_{b}=\mathfrak{m}_{b0}+_{i\in
I_{b}}\mathfrak{n}_{i}$

Taking $I:=I_{a}\uplus I_{b}$ and $\Phi_{0}:=\Phi_{a0}+\Phi_{b0}$ and
$(\Psi_{i})_{i\in I}:=(\Psi_{i})_{i\in I_{a}\uplus I_{b}}$ and
$\Gamma_{0}:=\Gamma_{a0}+\Gamma_{b0}$ and $(\Delta_{i})_{i\in
I}:=(\Delta_{i})_{i\in I_{a}\uplus I_{b}}$ and
$\mathfrak{m}_{0}:=[\texttt{B}]+\mathfrak{m}_{a0}+\mathfrak{m}_{b0}$ and
$(\mathfrak{n}_{i})_{i\in I}:=(\mathfrak{n}_{i})_{i\in I_{a}\uplus I_{b}}$ and
$(\mathcal{S}_{i})_{i\in I}:=(\mathcal{S}_{i})_{i\in I_{a}\uplus I_{b}}$, we
have:

    1. 1.

$\pi\rhd\Phi_{a0}+\Phi_{b0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{I_{a}\uplus
I_{b}};\Gamma_{a0}+\Gamma_{b0}\vdash^{[\texttt{B}]+\mathfrak{m}_{a0}+\mathfrak{m}_{b0}}s^{\prime}\,u^{\prime}:\mathcal{T}$,
by applying rule t-app to $\pi_{a}$ and $\pi_{b}$, given
$\mathcal{U}^{?}\lhd\mathcal{U}$

    2. 2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I_{a}\uplus I_{b}}$ as the result of applying Lemma 4 to $(\zeta_{i})_{i\in
I_{a}}$ and $(\zeta_{i})_{i\in I_{b}}$

    3. 3.

$\Phi=\Phi_{a}+\Phi_{b}=\Phi_{a0}+\Phi_{b0}+_{I_{a}\uplus
I_{b}}\Psi_{i}=\Phi_{0}+_{i\in I}\Psi_{i}$ and
$\Gamma=\Gamma_{a}+\Gamma_{b}=\Gamma_{a0}+\Gamma_{b0}+_{I_{a}\uplus
I_{b}}\Delta_{i}=\Gamma_{0}+_{i\in I}\Delta_{i}$ and
$\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}=[\texttt{B}]+\mathfrak{m}_{a0}+\mathfrak{m}_{b0}+_{I_{a}\uplus
I_{b}}\mathfrak{n}_{i}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{n}_{i}$

  * •

t-zero. Analogous to case t-var1.

  * •

t-succ. Then
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(u):[\mathbb{S}(\mathcal{N}_{j})]^{\mathsf{nat}}_{j\in
J}$, where $\mathcal{T}=[\mathbb{S}(\mathcal{N}_{j})]^{\mathsf{nat}}_{j\in
J}$. Then $t=\mathbf{S}(u^{\prime})$, with $u=u^{\prime}\\{x:=q\\}$. The
judgment is derived from
$\pi^{\prime}_{0}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}u:\mathcal{N}$, where
$\mathcal{N}=+_{j\in J}\mathcal{N}_{j}$. We can apply the IH on
$\pi^{\prime}_{0}$, yielding that there exist a finite set $I$, family
contexts $\Phi_{0}$ and $(\Psi_{i})_{i\in I}$, typing contexts $\Gamma_{0}$
and $(\Delta_{i})_{i\in I}$, multi-counters $\mathfrak{m}_{0}$ and
$(\mathfrak{n}_{i})_{i\in I}$ and multitypes $(\mathcal{S}_{i})_{i\in I}$ such
that:

    1. 1’.

$\pi^{\prime}_{0}\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}_{0}}u^{\prime}:\mathcal{N}$, where
$\mathcal{N}=+_{j\in J}\mathcal{N}_{j}$

    2. 2’.

$(\zeta_{0i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I}$

    3. 3’.

$\Phi=\Phi_{0}+_{i\in I}\Psi_{i}$ and $\Gamma=\Gamma_{0}+_{i\in I}\Delta_{i}$
and $\mathfrak{m}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{n}_{i}$

By taking $I$ and $\Phi_{0}$ and $(\Psi_{i})_{i\in I}$ and $\Gamma_{0}$ and
$(\Delta_{i})_{i\in I}$ and $\mathfrak{m}_{0}$ and $(\mathfrak{n}_{i})_{i\in
I}$ and $(\mathcal{S}_{i})_{i\in I}$ from the IH, we obtain
$\pi\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}+_{i\in
I}\Delta_{i}\vdash^{\mathfrak{m}_{0}}\mathbf{S}(u^{\prime}):[\mathbb{S}(\mathcal{N}_{j})]^{\mathsf{nat}}_{j\in
J}$ by applying rule t-succ with $\pi_{0}$ as premise, and the condition in
Item 2 holds by letting $\zeta_{i}:=\zeta_{i0}$ for all ${i\in I}$. The
conditions in Item 3 hold by the IH.

  * •

t-ifZero. Analogous to case t-app.

  * •

t-ifSucc. Then
$\pi^{\prime}\rhd\Phi_{a}+\Phi_{b};\Gamma_{a}+\Gamma_{b}\vdash^{[\texttt{IS}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}}\mathsf{if}(s,u,y.\,r):\mathcal{T}$,
where $\Phi=\Phi_{a}+\Phi_{b}$ and $\Gamma=\Gamma_{a}+\Gamma_{b}$ and
$\mathfrak{m}=[\texttt{IS}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}$. Then
$t=\mathsf{if}(s^{\prime},u^{\prime},y.\,r^{\prime})$, with
$s=s^{\prime}\\{x:=q\\}$ and $u=u^{\prime}\\{x:=q\\}$ and
$r=r^{\prime}\\{x:=q\\}$. The judgment is derived from
$\pi^{\prime}_{a}\rhd\Phi_{a};\Gamma_{a}\vdash^{\mathfrak{m}_{a}}s:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$
and
$\pi^{\prime}_{b}\rhd\Phi_{b};\Gamma_{b},y:\mathcal{N}^{?}\vdash^{\mathfrak{m}_{b}}r:\mathcal{T}$,
where $\mathcal{N}^{?}\lhd\mathcal{N}$. We can apply the IH on
$\pi^{\prime}_{a}$, yielding that there exist a finite set $I_{a}$, family
contexts $\Phi_{a0}$ and $(\Psi_{i})_{i\in I_{a}}$, typing contexts
$\Gamma_{a0}$ and $(\Delta_{i})_{i\in I_{a}}$, multi-counters
$\mathfrak{m}_{a0}$ and $(\mathfrak{n}_{i})_{i\in I_{a}}$ and multitypes
$(\mathcal{S}_{i})_{i\in I_{a}}$ such that:

    1. a.1.

$\pi_{a}\rhd\Phi_{a0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I_{a}};\Gamma_{a0}\vdash^{\mathfrak{m}_{a0}}s^{\prime}:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$

    2. a.2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I_{a}}$

    3. a.3.

$\Phi_{a}=\Phi_{a0}+_{i\in I_{a}}\Psi_{i}$ and $\Gamma_{a}=\Gamma_{a0}+_{i\in
I_{a}}\Delta_{i}$ and $\mathfrak{m}_{a}=\mathfrak{m}_{a0}+_{i\in
I_{a}}\mathfrak{n}_{i}$

And we can apply the IH on $\pi^{\prime}_{b}$, yielding that there exist a
finite set $I_{b}$, family contexts $\Phi_{b0}$ and $(\Psi_{i})_{i\in I_{b}}$,
typing contexts $\Gamma_{b0}$ and $(\Delta_{i})_{i\in I_{b}}$, multi-counters
$\mathfrak{m}_{b0}$ and $(\mathfrak{n}_{i})_{i\in I_{b}}$ and multitypes
$(\mathcal{S}_{i})_{i\in I_{b}}$ such that:

    1. b.1.

$\pi_{b}\rhd\Phi_{b0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I_{b}};\Gamma_{b0},y:\mathcal{N}^{?}\vdash^{\mathfrak{m}_{b0}}r^{\prime}:\mathcal{T}$

    2. b.2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I_{b}}$

    3. b.3.

$\Phi_{b}=\Phi_{b0}+_{i\in I_{b}}\Psi_{i}$ and
$\Gamma_{b},y:\mathcal{N}^{?}=\Gamma_{b0},y:\mathcal{N}^{?}+_{i\in
I_{b}}\Delta_{i}$ and $\mathfrak{m}_{b}=\mathfrak{m}_{b0}+_{i\in
I_{b}}\mathfrak{n}_{i}$. Note that it is not necessary to split
$\mathcal{N}^{?}_{j}$ since we may assume $y\notin\mathsf{fv}(q)$ by
$\alpha$-conversion, so $y\notin\mathsf{dom}(+_{i\in I_{b}}\Delta_{i})$ by
Lemma 2.

Taking $I:=I_{a}\uplus I_{b}$ and $\Phi_{0}:=\Phi_{a0}+\Phi_{b0}$ and
$(\Psi_{i})_{i\in I}:=(\Psi_{i})_{i\in I_{a}\uplus I_{b}}$ and
$\Gamma_{0}:=\Gamma_{a0}+\Gamma_{b0}$ and $(\Delta_{i})_{i\in
I}:=(\Delta_{i})_{i\in I_{a}\uplus I_{b}}$ and
$\mathfrak{m}_{0}:=[\texttt{IS}]+\mathfrak{m}_{a0}+\mathfrak{m}_{b0}$ and
$(\mathfrak{n}_{i})_{i\in I}:=(\mathfrak{n}_{i})_{i\in I_{a}\uplus I_{b}}$ and
$(\mathcal{S}_{i})_{i\in I}:=(\mathcal{S}_{i})_{i\in I_{a}\uplus I_{b}}$, we
have:

    1. 1.

$\pi\rhd\Phi_{a0}+\Phi_{b0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{I_{a}\uplus
I_{b}};\Gamma_{a0}+\Gamma_{b0}\vdash^{[\texttt{IS}]+\mathfrak{m}_{a0}+\mathfrak{m}_{b0}}\mathsf{if}(s^{\prime},u^{\prime},y.\,r^{\prime}):\mathcal{T}$,
by applying rule t-ifSucc to $\pi_{a}$ and $\pi_{b}$, given
$\mathcal{U}^{?}\lhd\mathcal{U}$

    2. 2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I_{a}\uplus I_{b}}$ as the result of applying Lemma 4 to $(\zeta_{i})_{i\in
I_{a}}$ and $(\zeta_{i})_{i\in I_{b}}$

    3. 3.

$\Phi=\Phi_{a}+\Phi_{b}=\Phi_{a0}+\Phi_{b0}+_{I_{a}\uplus
I_{b}}\Psi_{i}=\Phi_{0}+_{i\in I}\Psi_{i}$ and
$\Gamma=\Gamma_{a}+\Gamma_{b}=\Gamma_{a0}+\Gamma_{b0}+_{I_{a}\uplus
I_{b}}\Delta_{i}=\Gamma_{0}+_{i\in I}\Delta_{i}$ and
$\mathfrak{m}=[\texttt{IS}]+\mathfrak{m}_{a}+\mathfrak{m}_{b}=[\texttt{IS}]+\mathfrak{m}_{a0}+\mathfrak{m}_{b0}+_{I_{a}\uplus
I_{b}}\mathfrak{n}_{i}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{n}_{i}$

  * •

t-fix. Then $\pi^{\prime}\rhd\Phi^{\prime}+_{j\in
J}\Phi^{\prime}_{j};\Gamma^{\prime}+_{j\in
J}\Gamma^{\prime}_{j}\vdash^{[\texttt{F}]+\mathfrak{m}^{\prime}+_{j\in
J}\mathfrak{m}^{\prime}_{j}}\mathsf{fix}\,y.\,s:\mathcal{T}$, where
$\Phi=\Phi^{\prime}+_{j\in J}\Phi^{\prime}_{j}$ and
$\Gamma=\Gamma^{\prime}+_{j\in J}\Gamma^{\prime}_{j}$ and
$\mathfrak{m}=[\texttt{F}]+\mathfrak{m}^{\prime}+_{j\in
J}\mathfrak{m}^{\prime}_{j}$. Then $t=\mathsf{fix}\,y.\,s^{\prime}$, with
$s=s^{\prime}\\{x:=q\\}$. The judgment is derived from
$\pi^{\prime}_{0}\rhd\Phi^{\prime},y:\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in
J};\Gamma^{\prime}\vdash^{\mathfrak{m}^{\prime}}s:\mathcal{T}$ and
$(\pi^{\prime}_{j}\rhd\Phi^{\prime}_{j};\Gamma^{\prime}_{j}\vdash^{\mathfrak{m}^{\prime}_{j}}\mathsf{fix}\,y.\,s:\mathcal{U}_{j})_{j\in
J}$. We can apply IH on $s$, yielding that there exist a finite set
$I^{\prime}$, family contexts $\Phi^{\prime}_{0}$ and
$(\Psi^{\prime}_{i})_{i\in I^{\prime}}$, typing contexts $\Gamma^{\prime}_{0}$
and $(\Delta^{\prime}_{i})_{i\in I^{\prime}}$, multi-counters
$\mathfrak{m}^{\prime}_{0}$ and $(\mathfrak{n}^{\prime}_{i})_{i\in
I^{\prime}}$ and multitypes $(\mathcal{S}_{i})_{i\in I^{\prime}}$ such that:

    1. 1’.

$\pi_{0}\rhd\Phi^{\prime}_{0},y:\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in
J},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I^{\prime}};\Gamma^{\prime}_{0}\vdash^{\mathfrak{m}^{\prime}_{0}}s^{\prime}:\mathcal{T}$

    2. 2’.

$(\zeta_{i}\rhd\Psi^{\prime}_{i};\Delta^{\prime}_{i}\vdash^{\mathfrak{m}^{\prime}_{i}}q:\mathcal{S}_{i})_{i\in
I^{\prime}}$

    3. 3’.

$\Phi^{\prime},y:\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in
J}=\Phi^{\prime}_{0},y:\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in J}+_{i\in
I^{\prime}}\Psi^{\prime}_{i}$ and $\Gamma^{\prime}=\Gamma^{\prime}_{0}+_{i\in
I^{\prime}}\Delta^{\prime}_{i}$ and
$\mathfrak{m}^{\prime}=\mathfrak{m}^{\prime}_{0}+_{i\in
I^{\prime}}\mathfrak{n}^{\prime}_{i}$. Note that it is not necessary to split
$\\{\\!\\!\\{\mathcal{U}_{j}\\}\\!\\!\\}_{j\in J}$ since may assume
$y\notin\mathsf{fv}(q)$ by $\alpha$-conversion, so
$y\notin\mathsf{dom}(+_{i\in I^{\prime}}\Psi_{i})$ by Lemma 2.

Since the conclusion of $\pi^{\prime}_{j}$ is smaller than (1) for all ${j\in
J}$, we can then apply the IH on $(\pi^{\prime}_{j})_{j\in J}$, yielding that
for each ${j\in J}$, there exist a finite set $I^{\prime}_{j}$, family
contexts $\Phi^{\prime}_{j0}$ and $(\Psi^{\prime}_{i})_{i\in I^{\prime}_{j}}$,
typing contexts $\Gamma^{\prime}_{j0}$ and $(\Delta^{\prime}_{i})_{i\in
I^{\prime}_{j}}$, multi-counters $\mathfrak{m}^{\prime}_{j0}$ and
$(\mathfrak{n}^{\prime}_{i})_{i\in I^{\prime}_{j}}$ and multitypes
$(\mathcal{S}_{i})_{i\in I^{\prime}_{j}}$ such that:

    1. j.1.

$\pi_{j}\rhd\Phi^{\prime}_{j0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I^{\prime}_{j}};\Gamma^{\prime}_{j0}\vdash^{\mathfrak{m}^{\prime}_{j0}}\mathsf{fix}\,y.\,s^{\prime}:\mathcal{U}_{j}$

    2. j.2.

$(\zeta_{i}\rhd\Psi^{\prime}_{i};\Delta^{\prime}_{i}\vdash^{\mathfrak{m}^{\prime}_{i}}q:\mathcal{S}_{i})_{i\in
I^{\prime}_{j}}$

    3. j.3.

$\Phi=\Phi_{j0}+_{i\in I_{j}}\Psi_{i}$ and $\Gamma=\Gamma_{j0}+_{i\in
I_{j}}\Delta_{i}$ and $\mathfrak{m}=\mathfrak{m}_{j0}+_{i\in
I_{j}}\mathfrak{n}_{i}$

Taking $I:=I^{\prime}\uplus_{j\in J}I^{\prime}_{j}$ and
$\Phi_{0}:=\Phi^{\prime}_{0}+_{j\in J}\Phi^{\prime}_{j0}$ and
$(\Psi_{i})_{i\in I}:=(\Psi^{\prime}_{i})_{I^{\prime}\uplus_{j\in
J}I^{\prime}_{j}}$ and $\Gamma_{0}:=\Gamma^{\prime}_{0}+_{j\in
J}\Gamma^{\prime}_{j0}$ and $(\Delta_{i})_{i\in
I}:=(\Delta^{\prime}_{i})_{I^{\prime}\uplus_{j\in J}I^{\prime}_{j}}$ and
$\mathfrak{m}_{0}:=[\texttt{F}]+\mathfrak{m}^{\prime}_{0}+_{j\in
J}\mathfrak{m}^{\prime}_{j0}$ and $(\mathfrak{n}_{i})_{i\in
I}:=(\mathfrak{n}^{\prime}_{i})_{I^{\prime}\uplus_{j\in J}I^{\prime}_{j}}$ and
and $(\mathcal{S}_{i})_{i\in I}:=(\mathcal{S}_{i})_{I^{\prime}\uplus_{j\in
J}I^{\prime}_{j}}$ such that:

    1. 1.

$\pi\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}_{0}}\mathsf{fix}\,y.\,s^{\prime}:\mathcal{T}$,
by applying rule t-fix to $\pi_{0}$ and $(\pi_{j})_{j\in J}$

    2. 2.

$(\zeta_{i}\rhd\Psi_{i};\Delta_{i}\vdash^{\mathfrak{n}_{i}}q:\mathcal{S}_{i})_{i\in
I}$, as the result of applying Lemma 4 to $(\zeta_{i})_{i\in I^{\prime}}$ and
$(\zeta_{i})_{i\in I_{j}}$ for all ${j\in J}$

    3. 3.

$\Phi=\Phi^{\prime}+_{j\in J}\Phi^{\prime}_{j}=\Phi^{\prime}_{0}+_{j\in
J}\Phi^{\prime}_{j0}+_{I^{\prime}\uplus_{j\in
J}I^{\prime}_{j}}(\Psi^{\prime}_{i})_{I^{\prime}\uplus_{j\in
J}I^{\prime}_{j}}=\Phi_{0}+_{i\in I}\Psi_{i}$ and
$\Gamma=\Gamma^{\prime}+_{j\in
J}\Gamma^{\prime}_{j}=\Gamma^{\prime}_{0}+_{j\in
J}\Gamma^{\prime}_{j0}+_{I^{\prime}\uplus_{j\in
J}I^{\prime}_{j}}(\Delta^{\prime}_{i})_{I^{\prime}\uplus_{j\in
J}I^{\prime}_{j}}=\Gamma_{0}+_{i\in I}\Delta_{i}$ and
$\mathfrak{m}_{0}=[\texttt{F}]+\mathfrak{m}^{\prime}+_{j\in
J}\mathfrak{m}^{\prime}_{j}=\mathfrak{m}^{\prime}_{0}+_{j\in
J}\mathfrak{m}^{\prime}_{j0}+_{I^{\prime}\uplus_{j\in
J}I^{\prime}_{j}}(\mathfrak{n}^{\prime}_{i})_{I^{\prime}\uplus_{j\in
J}I^{\prime}_{j}}=\mathfrak{m}_{0}+_{i\in I}\mathfrak{n}_{i}$

∎

*

###### Proof.

We proceed by induction on the derivation of $t\to_{\rho}t^{\prime}$.

  1. 1.

r-beta. Then $t=(\lambda
x.\,s)\,\mathbf{v}\to_{\texttt{B}}s\\{x:=\mathbf{v}\\}=t^{\prime}$, with
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}s\\{x:=\mathbf{v}\\}:\mathcal{T}$.
By Lemmas for Completeness, there exist $\Phi_{1}$, $\Phi_{2}$, $\Gamma_{1}$,
$\Gamma_{2}$, $\mathfrak{m}^{\prime}_{1}$, $\mathfrak{m}^{\prime}_{2}$,
$\mathcal{S}^{?}$ and $\mathcal{S}$ such that $\Phi=\Phi_{1}+\Phi_{2}$ and
$\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}^{\prime}=\mathfrak{m}^{\prime}_{1}+\mathfrak{m}^{\prime}_{2}$
and $\mathcal{S}^{?}\lhd\mathcal{S}$ and
$\pi_{0}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}^{\prime}_{1}}s:\mathcal{T}$
and
$\zeta\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}^{\prime}_{2}}\mathbf{v}:\mathcal{S}$
hold. Hence we build the derivation $\pi$ as:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
2.44878pt\hbox{$\displaystyle\penalty
1\pi_{0}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}^{\prime}_{1}}s:\mathcal{T}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=99.95265pt\hbox{\kern
3.00003pt$\texttt{{t-abs}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}^{\prime}_{1}}\lambda
x.\,s:[\mathcal{S}^{?}\to\mathcal{T}]^{\mathsf{abs}}$}}}}\hskip 5.0pt plus
1.0fil\penalty 2\end{array}\mathcal{S}^{?}\lhd\mathcal{S}\hskip
14.22636pt\zeta\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}^{\prime}_{2}}\mathbf{v}:\mathcal{S}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=267.03624pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
88.09067pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{[\texttt{B}]+\mathfrak{m}^{\prime}}(\lambda
x.\,s)\,\mathbf{v}:\mathcal{T}$}}}}\end{array}$

  2. 2.

r-if0. Then $t=\mathsf{if}({\bf
0},t^{\prime},x.\,s)\to_{\texttt{I0}}t^{\prime}$ with
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}t^{\prime}:\mathcal{T}$,
and we build the derivation $\pi$ as:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
22.2666pt\hbox{$\displaystyle\penalty 1\vphantom{{}^{@}}$}}\hskip 0.0pt plus
0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=48.88876pt\hbox{\kern
3.00003pt$\texttt{{t-zero}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\varnothing;\varnothing\vdash^{[\,]}{\bf
0}:[\mathbb{0}]$}}}}\hskip 5.0pt plus 1.0fil\penalty
2\end{array}\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}t^{\prime}:\mathcal{T}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=182.87889pt\hbox{\kern
3.00003pt$\texttt{{t-ifZero}}$}}}\hbox{\kern
38.1476pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{[\texttt{I0}]+\mathfrak{m}^{\prime}}\mathsf{if}({\bf
0},t^{\prime},x.\,s):\mathcal{T}$}}}}\end{array}$

  3. 3.

r-ifS. Then
$t=\mathsf{if}(\mathbf{S}(\mathbf{k}),s,x.\,u)\to_{\texttt{IS}}u\\{x:=\mathbf{k}\\}=t^{\prime}$
with
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}u\\{x:=\mathbf{k}\\}:\mathcal{T}$.
By Lemmas for Completeness there exist family contexts $\Phi_{1}$, $\Phi_{2}$,
typing contexts $\Gamma_{1}$, $\Gamma_{2}$, multi-counters
$\mathfrak{m}^{\prime}_{1}$, $\mathfrak{m}^{\prime}_{2}$, an optional
multitype $\mathcal{S}^{?}$, and a multitype $\mathcal{S}$ such that
$\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}^{\prime}=\mathfrak{m}^{\prime}_{1}+\mathfrak{m}^{\prime}_{2}$
and $\mathcal{S}^{?}\lhd\mathcal{S}$ and
$\pi_{0}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}^{\prime}_{1}}u:\mathcal{T}$
$\zeta\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}^{\prime}_{2}}\mathbf{k}:\mathcal{S}$.
Moreover $\mathcal{S}$ is of the form $\mathcal{N}$ by Remark 1. Hence we
build $\pi$ as:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty 1\begin{array}[]{c}\hskip 5.0pt plus
1.0fil{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus 0.0001fil\hbox{\kern
10.59029pt\hbox{$\displaystyle\penalty
1\zeta\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}^{\prime}_{2}}\mathbf{k}:\mathcal{S}$}}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=86.56332pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}^{\prime}_{2}}\mathbf{S}(\mathbf{k}):[\mathbb{S}(\mathcal{S})]$}}}}\hskip
5.0pt plus 1.0fil\penalty 2\end{array}\mathcal{S}^{?}\lhd\mathcal{S}\hskip
14.22636pt\pi_{0}\rhd\Phi_{1};\Gamma_{1},x:\mathcal{S}^{?}\vdash^{\mathfrak{m}^{\prime}_{1}}u:\mathcal{T}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=288.24521pt\hbox{\kern
3.00003pt$\texttt{{t-ifSucc}}$}}}\hbox{\kern
83.58289pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{[\texttt{IS}]+\mathfrak{m}^{\prime}}\mathsf{if}(\mathbf{S}(\mathbf{k}),s,x.\,u):\mathcal{T}$}}}}\end{array}$

  4. 4.

r-fix. Then
$t=\mathsf{fix}\,x.\,s\to_{\texttt{F}}s\\{x:=\mathsf{fix}\,x.\,s\\}=t^{\prime}$
with
$\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}s\\{x:=\mathsf{fix}\,x.\,s\\}:\mathcal{T}$.
By Lemmas for Completeness, there exist a finite set $I$, family contexts
$\Phi_{0}$, $(\Phi_{i})_{i\in I}$, typing contexts $\Gamma_{0}$,
$(\Gamma_{i})_{i\in I}$, multi-counters $\mathfrak{m}^{\prime}_{0}$,
$(\mathfrak{m}^{\prime}_{i})_{i\in I}$, and multitypes
$(\mathcal{S}_{i})_{i\in I}$ such that $\Phi=\Phi_{0}+_{i\in I}\Phi_{i}$ and
$\Gamma=\Gamma_{0}+_{i\in I}\Gamma_{i}$ and
$\mathfrak{m}^{\prime}=\mathfrak{m}^{\prime}_{0}+_{i\in
I}\mathfrak{m}^{\prime}_{i}$, and such that
$\pi_{0}\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}^{\prime}_{0}}s:\mathcal{T}$ and
$\zeta_{i}\rhd\Phi_{i};\Gamma_{i}\vdash^{\mathfrak{m}^{\prime}_{i}}\mathsf{fix}\,x.\,s:\mathcal{S}_{i}$
hold for each ${i\in I}$. Hence we build $\pi$ as:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\pi_{0}\rhd\Phi_{0},x:\\{\\!\\!\\{\mathcal{S}_{i}\\}\\!\\!\\}_{i\in
I};\Gamma_{0}\vdash^{\mathfrak{m}^{\prime}_{0}}s:\mathcal{T}\hskip
14.22636pt(\pi_{i}\rhd\Phi_{i};\Gamma_{i}\vdash^{\mathfrak{m}^{\prime}_{i}}\mathsf{fix}\,x.\,s:\mathcal{S}_{i})_{i\in
I}$}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=240.19951pt\hbox{\kern
3.00003pt$\texttt{{t-fix}}$}}}\hbox{\kern
77.3279pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{[\texttt{F}]+\mathfrak{m}^{\prime}}\mathsf{fix}\,x.\,s:\mathcal{T}$}}}}\end{array}$

  5. 5.

r-appL. Then $t=s\,u\to_{\rho}s^{\prime}\,u=t^{\prime}$, which is derived from
$s\to_{\rho}s^{\prime}$. Moreover, we have
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}s^{\prime}\,u:\mathcal{T}$,
which can only be derived by rule t-app, thus $\pi^{\prime}$ has the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}^{\prime}_{1}}s^{\prime}:[\mathcal{S}^{?}\to\mathcal{T}]^{\mathsf{abs}}\hskip
14.22636pt(1)\ \mathcal{S}^{?}\lhd\mathcal{S}\hskip
14.22636pt\pi_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}^{\prime}_{2}}u:\mathcal{S}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=219.32953pt\hbox{\kern
3.00003pt$\texttt{{t-app}}$}}}\hbox{\kern
48.67545pt\hbox{$\displaystyle\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{B}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}^{\prime}_{2}}s^{\prime}\,u:\mathcal{T}$}}}}\end{array}$

where $\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}^{\prime}=[\texttt{B}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}^{\prime}_{2}$.
By the IH on $s\to_{\rho}s^{\prime}$ there exists $\mathfrak{m}_{1}$ such that
$\mathfrak{m}_{1}=[\rho]+\mathfrak{m}^{\prime}_{1}$, and
$\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}_{1}}s:[\mathcal{S}^{?}\to\mathcal{T}]^{\mathsf{abs}}$.
Applying rule t-app with $\pi_{1}$, (1) and $\pi_{2}$ as premises, we conclude
$\pi\rhd\Phi_{1}+\Phi_{2};\Gamma_{1}+\Gamma_{2}\vdash^{[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}^{\prime}_{2}}s\,u:\mathcal{T}$,
where $\mathfrak{m}=[\texttt{B}]+\mathfrak{m}_{1}+\mathfrak{m}^{\prime}_{2}$
and verifies
$\mathfrak{m}=[\texttt{B}]+[\rho]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}^{\prime}_{2}=[\rho]+\mathfrak{m}^{\prime}$.

  6. 6.

r-appR. Analogous to the previous case.

  7. 7.

r-succ. Then $t=\mathbf{S}(s)\to_{\rho}\mathbf{S}(s^{\prime})=t^{\prime}$,
which is derived from $s\to_{\rho}s^{\prime}$. Moreover, we have
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}\mathbf{S}(s^{\prime}):\mathcal{T}$,
which can only be derived by rule t-succ, thus $\pi^{\prime}$ has the form:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{\kern 14.76256pt\hbox{$\displaystyle\penalty
1\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}s^{\prime}:+_{i\in
I}\mathcal{M}_{i}$}}\hskip 0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=98.32pt\hbox{\kern
3.00003pt$\texttt{{t-succ}}$}}}\hbox{\kern
0.0pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}\mathbf{S}(s^{\prime}):[\mathbb{S}(\mathcal{M}_{i})]^{\mathsf{nat}}_{i\in
I}$}}}}\end{array}$

where $\mathcal{T}=[\mathbb{S}(\mathcal{M}_{i})]^{\mathsf{nat}}_{i\in I}$. By
the IH on $s\to_{\rho}s^{\prime}$, there exists $\mathfrak{m}$ such that
$\mathfrak{m}=[\rho]+\mathfrak{m}^{\prime}$, and
$\pi_{0}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}s:+_{i\in I}\mathcal{M}_{i}$.
Applying rule t-succ to $\pi_{0}$, we conclude with
$\pi\rhd\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(s):[\mathbb{S}(\mathcal{M}_{i})]^{\mathsf{nat}}_{i\in
I}$, where $\mathfrak{m}$ verifies $\mathfrak{m}=[\rho]+\mathfrak{m}^{\prime}$
by the IH.

  8. 8.

r-if. Then
$t=\mathsf{if}(s,u,x.\,r)\to_{\rho}\mathsf{if}(s^{\prime},u,x.\,r)=t^{\prime}$
which is derived from $s\to_{\rho}s^{\prime}$. Moreover, we have
$\pi^{\prime}\rhd\Phi;\Gamma\vdash^{\mathfrak{m}^{\prime}}\mathsf{if}(s^{\prime},u,x.\,r):\mathcal{T}$.
We consider two subcases, depending on whether the conclusion of
$\pi^{\prime}$ is obtained from t-ifZero or t-ifSucc:

    1. 8.1

t-ifZero. Then there exist family contexts $\Phi_{1}$, $\Phi_{2}$, typing
contexts $\Gamma_{1}$, $\Gamma_{2}$, and multi-counters
$\mathfrak{m}^{\prime}_{1}$, $\mathfrak{m}^{\prime}_{2}$ such that
$\Phi=\Phi_{1}+\Phi_{2}$ and $\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}^{\prime}=[\texttt{I0}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}^{\prime}_{2}$,
and
$\pi^{\prime}_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}^{\prime}_{1}}s^{\prime}:[\mathbb{0}]$
and
$\pi^{\prime}_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}^{\prime}_{2}}u:\mathcal{T}$.
By the IH on $s\to_{\rho}s^{\prime}$, there exits $\mathfrak{m}_{1}$ such that
$\mathfrak{m}_{1}=[\rho]+\mathfrak{m}^{\prime}_{1}$, and
$\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{[\rho]+\mathfrak{m}^{\prime}_{1}}s:[\mathbb{0}]$.
Hence we build $\pi$ as:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{[\rho]+\mathfrak{m}^{\prime}_{1}}s:[\mathbb{0}]^{\mathsf{nat}}\hskip
14.22636pt\pi^{\prime}_{2}\rhd\Phi_{2};\Gamma_{2}\vdash^{\mathfrak{m}^{\prime}_{2}}u:\mathcal{T}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=180.84517pt\hbox{\kern
3.00003pt$\texttt{{t-ifZero}}$}}}\hbox{\kern
37.9128pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{[\rho]+\mathfrak{m}^{\prime}}\mathsf{if}(s,u,x.\,r):\mathcal{T}$}}}}\end{array}$

    2. 8.2

t-ifSucc. Then there exist family contexts $\Phi_{1}$, $\Phi_{2}$, typing
contexts $\Gamma_{1}$, $\Gamma_{2}$, multi-counters
$\mathfrak{m}^{\prime}_{1}$, $\mathfrak{m}^{\prime}_{2}$, an optional
$\mathsf{nat}$-multitype $\mathcal{N}^{?}$ and a $\mathsf{nat}$-multitype
$\mathcal{N}$ such that $\Phi=\Phi_{1}+\Phi_{2}$ and
$\Gamma=\Gamma_{1}+\Gamma_{2}$ and
$\mathfrak{m}^{\prime}=[\texttt{IS}]+\mathfrak{m}^{\prime}_{1}+\mathfrak{m}^{\prime}_{2}$
and (1) $\mathcal{N}^{?}\lhd\mathcal{N}$, and
$\pi^{\prime}_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{\mathfrak{m}^{\prime}_{1}}s^{\prime}:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$
and
$\pi^{\prime}_{2}\rhd\Phi_{2};\Gamma_{2},x:\mathcal{N}^{?}\vdash^{\mathfrak{m}^{\prime}_{2}}r:\mathcal{T}$.
By the IH on $s\to_{\rho}s^{\prime}$, there exists $\mathfrak{m}_{1}$ such
that $\mathfrak{m}_{1}=[\rho]+\mathfrak{m}^{\prime}_{1}$, and
$\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{[\rho]+\mathfrak{m}^{\prime}_{1}}s:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}$.
Hence we build $\pi$ as:

$\begin{array}[]{c}{tensy\vbox{\hbox spread0.0pt{\hskip 0.0pt plus
0.0001fil\hbox{$\displaystyle\penalty
1\pi_{1}\rhd\Phi_{1};\Gamma_{1}\vdash^{[\rho]+\mathfrak{m}^{\prime}_{1}}s:[\mathbb{S}(\mathcal{N})]^{\mathsf{nat}}\hskip
14.22636pt(1)\ \mathcal{N}^{?}\lhd\mathcal{N}\hskip
14.22636pt\pi^{\prime}_{2}\rhd\Phi_{2};\Gamma_{2},x:\mathcal{N}^{?}\vdash^{\mathfrak{m}^{\prime}_{2}}r:\mathcal{T}$}\hskip
0.0pt plus 0.0001fil}\hbox{\hbox{\kern 0.0pt\vrule
height=0.25002pt,depth=0.25002pt,width=279.02942pt\hbox{\kern
3.00003pt$\texttt{{t-ifSucc}}$}}}\hbox{\kern
87.00493pt\hbox{$\displaystyle\Phi;\Gamma\vdash^{[\rho]+\mathfrak{m}^{\prime}}\mathsf{if}(s,u,x.\,r):\mathcal{T}$}}}}\end{array}$

∎

*

###### Proof.

By induction on the derivation of $t\in\mathsf{NF}_{\nu}$. Recall cases nf-
app, nf-succ-stuck and nf-if do not apply since $\mathsf{stuck}$ is not a
proper nature.

  1. 1.

nf-abs. Then $t=\lambda x.\,s\in\mathsf{NF}_{\mathsf{abs}}$ and we can type
$t$ using t-abs.

  2. 2.

nf-zero. Then $t={\bf 0}\in\mathsf{NF}_{\mathsf{nat}}$ and we can type $t$
using t-zero.

  3. 3.

nf-succ-nat. Then $t=\mathbf{S}(u)\in\mathsf{NF}_{\mathsf{nat}}$ where
$u\in\mathsf{NF}_{\mathsf{nat}}$. By IH on $u\in\mathsf{NF}_{\mathsf{nat}}$,
$\Phi;\Gamma\vdash^{\mathfrak{m}}u:\mathcal{T}$. Moreover, since $u$ is a
normal form with $\mathsf{nat}$ nature, it must be the case that
$u=\mathbf{k}$, so by Remark 1, $\mathcal{T}$ is of the form $\mathcal{N}$,
which can be written as $+_{i\in I}\mathcal{N}_{i}$. Hence
$\Phi;\Gamma\vdash^{\mathfrak{m}}\mathbf{S}(u):[\mathbb{S}(\mathcal{N}_{i})]^{\mathsf{nat}}_{i\in
I}$ by applying t-succ. ∎

*

###### Proof.

($1\Rightarrow 2$) By induction on the size of $\mathfrak{m}$, analyzing
whether $t\in\mathsf{NF}_{\nu}$ or not.

  * •

If $t\in\mathsf{NF}_{\nu}$, then $t$ is of the form $\lambda x.\,s$, ${\bf
0}$, or $\mathbf{S}(\mathbf{k})$, given that $\nu$ is a proper nature. Hence
$t$ can only be derived by rule t-abs, t-zero, or t-succ respectively. In the
three cases we obtain $\mathfrak{m}=[\,]$ by Lemma 3, so taking $n=0$ we are
done.

  * •

If $t\notin\mathsf{NF}_{\nu}$. Then by Section 0.2 it must exist a term
$t^{\prime}$ and a rule name $\rho$ such that $t\to_{\rho}t^{\prime}$. By
Lemmas for Soundness there exists $\mathfrak{m}^{\prime}$ such that
$\mathfrak{m}=[\rho]+\mathfrak{m}^{\prime}$, and
$\varnothing;\varnothing\vdash^{\mathfrak{m}^{\prime}}t^{\prime}:[\,]^{\nu}$.
By IH on $\mathfrak{m}^{\prime}$, there exists a sequence of steps
$t^{\prime}\to_{\rho_{1}}t_{1}\ldots\to_{\rho_{n}}t_{n}$ where
$t_{n}\in\mathsf{NF}_{\nu}$ and
$\mathfrak{m}^{\prime}=[\rho_{1},\ldots,\rho_{n}]$. By joining this reduction
sequence with the reduction step $t\to_{\rho}t^{\prime}$ we have a reduction
sequence, $t\to_{\rho}t^{\prime}\to_{\rho_{1}}t_{1}\ldots\to_{\rho_{n}}t_{n}$,
and $\mathfrak{m}=[\rho]+[\rho_{1},\ldots,\rho_{n}]$, so we are done.

($2\Rightarrow 1$) By induction on $n$.

  1. 1.

$n=0$. Then $t\in\mathsf{NF}_{\nu}$, and $\mathfrak{m}=[\,]$. Therefore
$\varnothing;\varnothing\vdash^{[\,]}t:[\,]^{\nu}$ holds by Lemma 5.

  2. 2.

$n>0$, assuming the property holds for $n-1$. Taking the reduction sequence of
$(n-1)$ steps from $t_{1}$ to $t_{n}$, and
$\mathfrak{m}^{\prime}=[\rho_{2},\ldots,\rho_{n}]$ we can apply IH, yielding
$\varnothing;\varnothing\vdash^{\mathfrak{m}^{\prime}}t_{1}:[\,]^{\nu}$. Since
$t\to_{\rho_{1}}t_{1}$, then by Lemmas for Completeness we have
$\varnothing;\varnothing\vdash^{\mathfrak{m}}t:[\,]^{\nu}$, with
$\mathfrak{m}=[\rho_{1}]+\mathfrak{m}^{\prime}$, as stated in the hypothesis,
so we are done.

∎


# Nuij Sequences for Gårding Hyperbolic Polynomials

Tristan Hasson  Tristan Hasson, Department of Mathematical Sciences,
University of Durham, Durham DH1 3LE, United Kingdom
<EMAIL_ADDRESS>
###### Abstract.

Hyperbolic polynomials were first introduced by Gårding in 1959 in [2]. The
space of this type of polynomial was studied by Nuij and various results were
given in [4]. Following the work of Kurdyka and Paunescu in [3], this paper
gives a result on hyperbolicity preserving operators on the space of
polynomials.

###### 2010 Mathematics Subject Classification:

53C24

## Main Result

We begin by giving the definition of a hyperbolic polynomial to fix notation.

######  Definition 1.

Let $P(x_{1},\dots,x_{n})$ be a degree $m$ homogeneous polynomial on
$\mathbb{R}^{n}$. If for some $e\in\mathbb{R}^{n}$ the univariate polynomial
$t\mapsto P(x+te)$ has only real roots for all $x\in\mathbb{R}^{n}$, then we
say $P$ is hyperbolic with respect to $e$.

Nuij makes important use of a collection of hyperbolicity preserving operators
in his paper [4] to prove results on the space of hyperbolic polynomials.
Assume that $P$ is hyperbolic with respect to the $x_{n}$ direction, then
these operators are of the form:

$T_{k,s}P\coloneqq P+sx_{k}\frac{\partial P}{\partial x_{n}}$ (1)

where $s\in\mathbb{R}$ parameterises a collection of operators. In his paper
Nuij combines these first order operators to form ones with higher order
derivatives. For example in a 3 dimensional setting we could have

$T_{x,s}T_{x,s}T_{y,s}T_{y,s}=P+s(2x+2y)\frac{\partial P}{\partial
z}+s^{2}(x^{2}+4xy+y^{2})\frac{\partial^{2}P}{\partial z^{2}}\\\
+s^{3}(2x^{2}y+2xy^{2})\frac{\partial^{3}P}{\partial
z^{3}}+s^{4}x^{2}y^{2}\frac{\partial^{4}P}{\partial z^{4}}$ (2)

Note this bears resemblance to the construction of Nuij sequences from [3].
This motivates the following definition in the setting of Gårding’s hyperbolic
polynomials.

######  Definition 2.

Given any $P(x_{1},\dots,x_{n})$, a polynomial of degree $m$ hyperbolic with
respect to the $x_{n}$ direction, a sequence $a=(a_{1},\dots,a_{m})$ of
polynomials, where $a_{k}\in\mathbb{R}_{k}[x_{1},\dots,x_{n-1}]$, is a Gårding
Nuij sequence if the polynomial

$P_{a,s}(x_{1},\dots,x_{n})\coloneqq
P(x_{1},\dots,x_{n})+\sum_{k=1}^{m}a_{k}s^{k}\frac{\partial^{k}P(x_{1},\dots,x_{n})}{\partial
x_{n}^{k}}$ (3)

is hyperbolic with respect to $x_{n}$ for any $s\in\mathbb{R}$.

We now prove the following theorem giving a condition for any sequence of
homogenisation coefficients to give rise to a hyperbolicity preserving
operator.

######  Theorem 3.

A sequence $a=(a_{1},\dots,a_{m})$ where
$a_{k}\in\mathbb{R}_{k}[x_{1},\dots,x_{n-1}]$ is a Gårding Nuij sequence if
and only if

$Q_{a}(x_{1},\dots,x_{n})=x_{n}^{m}+\sum_{k=1}^{m}a_{k}\frac{\partial^{k}(x_{n}^{m})}{\partial
x_{n}^{k}}$ (4)

is a hyperbolic polynomial.

The proof of this theorem makes use of a result of [1]. We must first give the
definition of a stable polynomial before giving the statement of this result.

######  Definition 4.

Let $p\in\mathbb{C}[z_{1},\dots,z_{n}]$ be a degree $m$ polynomial, if for all
$(z_{1},\dots,z_{n})\in\mathbb{C}^{n}$ with $Im(z_{i})>0$ $1\leq i\leq n$ we
have $p(z_{1},\dots,z_{n})\neq 0$ then we say $p$ is stable.

######  Theorem 5.

Let $T:\mathbb{C}_{m}[z]\rightarrow\mathbb{C}_{m}[z]$ be a linear map. We
extend $T$ to a linear map
$\bar{T}:\mathbb{C}_{m}[z,w]\rightarrow\mathbb{C}_{m}[z,w]$ by setting
$\bar{T}(z^{k}w^{l})\coloneqq T(z^{k})w^{l}$. If $\bar{T}((z+w)^{d})$ is a
stable polynomial in two variables, then $T$ preserves stability.

We can now prove our main result. This proof is based on a proof from [3].

###### Proof of Theorem 3.

We begin with the easy direction, if $a$ is a Gårding Nuij sequence then
$Q_{a}$ is a hyperbolic polynomial. Now $Q_{a}$ is simply the Nuij sequence
construction acting upon the polynomial $x_{n}^{m}$, so since $P=x_{n}^{m}$ is
hyperbolic with respect to $x_{n}$, we have $Q_{a}$ is hyperbolic.

This leaves us to prove: if $Q_{a}$ is a hyperbolic polynomial, then $a$ is a
Gårding Nuij sequence. Define a map

$T_{a}(P)(x_{1},\dots,x_{n})\coloneqq
P(x_{1},\dots,x_{n})+\sum_{k=1}^{m}a_{k}\frac{\partial^{k}P(x_{1},\dots,x_{n})}{\partial
x_{n}^{k}}.$ (5)

We need to show that if $Q_{a}$ is hyperbolic then $T_{a}$ preserves
hyperbolicity.

Now, $T_{a}$ preserves hyperbolicity if for all $v=(v_{1},\dots,v_{n})$ fixed,
the univariate polynomial given by restricting $T_{a}(P)$ to the line through
$v$ in the direction $x_{n}$ has only real roots. Denote $T_{a}(P)$ restricted
to this line by

$T_{a_{v}}(P_{v})=T(P)(v_{1},\dots,v_{n-1},x_{n}),$ (6)

so $T_{a,v}:\mathbb{C}_{m}[z]\rightarrow\mathbb{C}_{m}[z]$ is a linear map.

Explicitly we have

$T_{a,v}(P-v)(x_{n})=P_{v}(x_{n})+\sum_{k=1}^{m}a_{k}(v_{1},\dots,v_{n-1})\frac{dP_{v}(x_{n})}{dx_{n}}$
(7)

and since the $v_{1},\dots,v_{n-1}$ are fixed, so is
$a_{k}(v_{1},\dots,v_{n-1})$ which we will denote $a_{k,v}$.

To show $T_{a}$ preserves hyperbolicity we will show
$T_{a,v}((z+w)^{d})=Q_{a}(z+w)$, to which we will be able to apply the result
of Theorem 5.

First consider $T_{a,v}$,

$\begin{split}T_{a,v}((z+w)^{d})&=T_{a,v}\Big{(}\sum_{i=0}^{d}\binom{d}{i}z^{i}w^{d-i}\Big{)}\\\
&=\sum_{i=0}^{d}\binom{d}{i}w^{d-i}T_{a,v}(z^{i}).\end{split}$ (8)

Now note that

$T_{a,v}(z^{i})=\sum_{j=0}^{i}a_{j,v}(z^{i})^{(j)}=\sum_{j=0}^{i}a_{j,v}\frac{i!}{(i-j)!}z^{i-j},$
(9)

so plugging this into the above we obtain

$\sum_{i=0}^{d}\binom{d}{i}w^{d-i}\Big{(}\sum_{j=0}^{i}a_{j,v}\frac{i!}{(i-j)!}z^{i-j}\Big{)}\\\
=\sum_{i=0}^{d}\binom{d!}{(d-i)!i!}w^{d-i}\Big{(}\sum_{j=0}^{i}a_{j,v}\frac{i!}{(i-j)!}z^{i-j}\Big{)}.$
(10)

Now we can pick out the expression that comes with each $a_{j,v}$,

$\sum_{i=j}^{d}\frac{d!}{(d-i)!i!}\frac{i!}{(i-j)!}z^{i-j}w^{d-i}$ (11)

and relabelling the index gives

$\sum_{k=0}^{d-j}\frac{d!}{(d-j-k)!k!}z^{k}w^{d-j-k}.$ (12)

Now we consider $Q_{a}(z+w)$, by definition we have

$Q_{a}(z+w)=\sum_{i=0}^{d}\frac{d!}{(d-i)!}a_{i,v}(z+w)^{d-i}.$ (13)

The coefficient of $a_{j}$ here is

$\begin{split}\frac{d!}{(d-j)!}(z+w)^{d-j}&=\frac{d!}{(d-j)!}\sum_{k=0}^{d-j}\binom{d-j}{k}z^{k}w^{d-j-k}\\\
&=\frac{d!}{(d-j)!}\sum_{k=0}^{d-j}\frac{(d-j)!}{(d-j-k)!k!}z^{k}w^{d-j-k}\\\
&=\sum_{k=0}^{d-j}\frac{d!}{(d-j-k)!k!}z^{k}w^{d-j-k}.\end{split}$ (14)

This is the same expression for the $a_{j,v}$ as in $T_{a,v}$ hence
$T_{a,v}((z+w)^{d})=Q_{a}(z+w)$.

Now since $Q_{a}(x_{n})$ has only real roots, we have that $Q_{a}(x_{n},w)$ is
a stable polynomial in two variables. Hence since
$T_{a,v}(x_{n},w)=Q_{a}(x_{n},w)$, we have $T_{a,v}$ preserves stability.
Restricting to real polynomials, $\mathbb{R}_{m}[x_{1},\dots,x_{n}]$, we have
that $T_{a,v}$ preserves real-rootedness. So for all $v\in\mathbb{R}^{n}$ we
have if $P$ restricted to the line through $v$ in the direction $x_{n}$ has
only real roots, then $T(P)$ restricted to the same line also has only real
roots. Hence $T$ preserves Gårding hyperbolicity and $a$ is a Gårding Nuij
sequence. ∎

######  Remark 6.

Note in this proof we set $s=1$ in the definition of the Gårding Nuij
sequence. A little more work is required to prove the theorem in generality.

## References

  * [1] Julius Borcea and Petter Brändén, _Pólya-Schur master theorems for circular domains and their boundaries_ , Annals of Mathematics 170 (2009), no. 1, 465–492.
  * [2] L. Gårding, _An inequality for hyperbolic polynomials_ , Journal of Mathematics and Mechanics 8 (6) (1959), 957–965.
  * [3] Krzysztof Kurdyka and Laurentiu Paunescu, _Nuij type pencils of hyperbolic polynomials_ , Canadian Mathematical Bulletin 60 (2017), no. 3, 561–570.
  * [4] Wim Nuij, _A note on hyperbolic polynomials_ , Mathematica Scandinavica 23 (1968), no. 1, 69–72.