$\Gamma=(\Gamma_{1}^{\prime}+\Gamma^{\prime}_{2}{{}_{|\Gamma^{\prime}_{1}}}+\Gamma^{\prime\prime}_{2}{{}_{|\Gamma^{\prime}_{1}}})$
&
$\Gamma^{\prime}=(\Gamma^{\prime\prime}_{1}+\Gamma^{\prime}_{2}{{}_{|\overline{\Gamma^{\prime}_{1}}}}+\Gamma^{\prime\prime}_{2}{{}_{|\overline{\Gamma^{\prime}_{1}}}})$)
$\displaystyle=\Gamma_{1}^{\prime}+(r_{1}\oplus
r_{2})\cdot\Delta+\Gamma^{\prime\prime}_{1}+(\Gamma^{\prime}_{2}{{}_{|\Gamma^{\prime}_{1}}}+\Gamma^{\prime}_{2}{{}_{|\overline{\Gamma^{\prime}_{1}}}})+(\Gamma^{\prime\prime}_{2}{{}_{|\Gamma^{\prime}_{1}}}+\Gamma^{\prime\prime}_{2}{{}_{|\overline{\Gamma^{\prime}_{1}}}})$
($\because$ $+$ associativity & commutativity)
$\displaystyle=\Gamma_{1}^{\prime}+(r_{1}\oplus
r_{2})\cdot\Delta+\Gamma^{\prime\prime}_{1}+\Gamma^{\prime}_{2}+\Gamma^{\prime\prime}_{2}$
($\because$ Lemma 2)
$\displaystyle=\Gamma_{1}^{\prime}+r_{1}\cdot\Delta+r_{2}\cdot\Delta+\Gamma^{\prime\prime}_{1}+\Gamma^{\prime}_{2}+\Gamma^{\prime\prime}_{2}$
($\because$ Lemma 5)
$\displaystyle=(\Gamma_{1}^{\prime}+r_{1}\cdot\Delta+\Gamma^{\prime\prime}_{1})+(\Gamma^{\prime}_{2}+r_{2}\cdot\Delta+\Gamma^{\prime\prime}_{2})$
($\because$ $+$ associativity and commutativity)

Thus, we obtain the conclusion of the lemma.

  * •

Case (weak)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime}\vdash
t:B\quad\vdash\Delta^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime}+[\Delta^{\prime}]_{0}\vdash
t:B\end{array}}$ (weak)

In this case, we know
$(\Gamma,x:[A]_{r},\Gamma^{\prime})=\Gamma^{\prime\prime}+[\Delta^{\prime}]_{0}$.
There are two cases where the versioned assumption $x:[A]_{r}$ is contained in
$[\Delta^{\prime}]_{0}$ and not included.

    * –

Suppose $(x:[A]_{r})\in[\Delta^{\prime}]_{0}$
We know $r=0$. Let $\Delta_{1}$ and $\Delta_{2}$ be typing context such that
$\Delta^{\prime}=(\Delta_{1},x:[A]_{0},\Delta_{2})$. The last derivation is
rewritten as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime}\vdash
t:B\quad\vdash\Delta_{1}+\Delta+\Delta_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime}+[\Delta_{1},x:[A]_{0},\Delta_{2}]_{0}\vdash
t:B\end{array}}$ (weak)

We compare the typing contexts between the conclusion of the lemma and that of
the above derivation to obtain the following:

$\displaystyle(\Gamma,x:[A]_{0},\Gamma^{\prime})$
$\displaystyle=\Gamma^{\prime\prime}+[\Delta_{1},x:[A]_{0},\Delta_{2}]_{0}$
($\because$ $\Delta^{\prime}=(\Delta_{1},x:[A]_{0},\Delta_{2})$)
$\displaystyle=\Gamma^{\prime\prime}+([\Delta_{1}]_{0},x:[A]_{0},[\Delta_{2}]_{0})$
($\because$ definiton of $[\Gamma]_{0}$)
$\displaystyle=(\Gamma^{\prime\prime}{{}_{|[\Delta_{2}]_{0}}}+[\Delta_{1}]_{0}),x:[A]_{0},(\Gamma^{\prime\prime}{{}_{|\overline{[\Delta_{2}]_{0}}}}+[\Delta_{2}]_{0})$
($\because$ Lemma 3 (2))

By the commutativity of ”,”, we can take $\Gamma$ and $\Gamma^{\prime}$
arbitrarily so that they satisfy the above equation. So here we know
$\Gamma=(\Gamma^{\prime\prime}{{}_{|[\Delta_{2}]_{0}}}+[\Delta_{1}]_{0})$ and
$\Gamma^{\prime}=(\Gamma^{\prime\prime}{{}_{|\overline{[\Delta_{2}]_{0}}}}+[\Delta_{2}]_{0})$.

We then apply the induction hypothesis to the premise of the last derivation
and reapply (weak) as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime}\vdash[t^{\prime}/x]t:B\quad\vdash\Delta_{1}+\Delta+\Delta_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime}+[\Delta_{1}+\Delta+\Delta_{2}]_{0}\vdash[t^{\prime}/x]t:B\end{array}}$
(weak)

where we choose $\Delta_{1}+\Delta+\Delta_{2}$ as the newly added typing
context. Since $x$ is unused by $t$, thus note that $[t^{\prime}/x]t=t$, the
conclusion of the above derivation is equivalent to the conclusion of the
lemma except for typing contexts.

Finally, we must show that
$(\Gamma+r\cdot\Delta+\Gamma^{\prime})=\Gamma^{\prime\prime}+[\Delta_{1}+\Delta+\Delta_{2}]_{0}$.

$\displaystyle(\Gamma+r\cdot\Delta+\Gamma^{\prime})$
$\displaystyle=(\Gamma^{\prime\prime}{{}_{|[\Delta_{2}]_{0}}}+[\Delta_{1}]_{0})+[\Delta]_{0}+(\Gamma^{\prime\prime}{{}_{|\overline{[\Delta_{2}]_{0}}}}+[\Delta_{2}]_{0})$
($\because$ $r=0$ &
$\Gamma=(\Gamma^{\prime\prime}{{}_{|[\Delta_{2}]_{0}}}+[\Delta_{1}]_{0})$ &
$\Gamma^{\prime}=(\Gamma^{\prime\prime}{{}_{|\overline{[\Delta_{2}]_{0}}}}+[\Delta_{2}]_{0})$)
$\displaystyle=(\Gamma^{\prime\prime}{{}_{|[\Delta_{2}]_{0}}}+\Gamma^{\prime\prime}{{}_{|\overline{[\Delta_{2}]_{0}}}})+([\Delta_{1}]_{0}+[\Delta]_{0}+[\Delta_{2}]_{0})$
($\because$ $+$ associativity and commutativity)
$\displaystyle=\Gamma^{\prime\prime}+([\Delta_{1}]_{0}+[\Delta]_{0}+[\Delta_{2}]_{0})$
($\because$ Lemma 2)
$\displaystyle=\Gamma^{\prime\prime}+[\Delta_{1}+\Delta+\Delta_{2}]_{0}$
($\because$ definition of $[\Gamma]_{0}$)

Thus, we obtain the conclusion of the lemma.

    * –

Suppose $(x:[A]_{r})\notin[\Delta^{\prime}]_{0}$
Let $\Gamma_{1}$ and $\Gamma_{2}$ be typing context such that
$\Gamma^{\prime\prime}=(\Gamma_{1},x:[A]_{r},\Gamma_{2})$. The last typing
derivation of $(\textsc{weak})$ is rewritten as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}(\Gamma_{1},x:[A]_{r},\Gamma_{2})\vdash
t:B\quad\vdash\Delta^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}(\Gamma_{1},x:[A]_{r},\Gamma_{2})+[\Delta^{\prime}]_{0}\vdash
t:B\end{array}}$ (weak)

We then compare the typing context between the conclusion of the lemma and
that of the that of above derivation as follows:

$\displaystyle(\Gamma,x:[A]_{r},\Gamma^{\prime})$
$\displaystyle=(\Gamma_{1},x:[A]_{r},\Gamma_{2})+[\Delta^{\prime}]_{0}$
$\displaystyle=(\Gamma_{1}+([\Delta^{\prime}]_{0}){{}_{|\Gamma_{1}}}),x:[A]_{r},(\Gamma_{2}+([\Delta^{\prime}]_{0}){{}_{|\overline{\Gamma_{1}}}})$
($\because$ Lemma 3 (1))

By the commutativity of ”,”, we can take $\Gamma$ and $\Gamma^{\prime}$
arbitrarily so that they satisfy the above equation. So here we know
$\Gamma=(\Gamma_{1}+([\Delta^{\prime}]_{0}){{}_{|\Gamma_{1}}})$ and
$\Gamma^{\prime}=(\Gamma_{2}+([\Delta^{\prime}]_{0}){{}_{|\overline{\Gamma_{1}}}})$.
We then apply the induction hypothesis to the premise of the last derivation
and reapply (weak) as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}+r\cdot\Delta+\Gamma_{2}\vdash[t^{\prime}/x]t:B\quad\vdash\Delta^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}(\Gamma_{1}+r\cdot\Delta+\Gamma_{2})+[\Delta^{\prime}]_{0}\vdash[t^{\prime}/x]t:B\end{array}}$
(weak)

The conclusion of the above derivation is equivalent to the conclusion of the
lemma except for the typing contexts. Finally, we must show that
$(\Gamma+r\cdot\Delta+\Gamma^{\prime})=(\Gamma_{1}+r\cdot\Delta+\Gamma_{2})+[\Delta^{\prime}]_{0}$.

$\displaystyle(\Gamma+r\cdot\Delta+\Gamma^{\prime})$
$\displaystyle=(\Gamma_{1}+([\Delta^{\prime}]_{0}){{}_{|\Gamma_{1}}})+r\cdot\Delta+(\Gamma_{2}+([\Delta^{\prime}]_{0}){{}_{|\overline{\Gamma_{1}}}})$
($\because$ $\Gamma=(\Gamma_{1}+([\Delta^{\prime}]_{0}){{}_{|\Gamma_{1}}})$ &
$\Gamma^{\prime}=(\Gamma_{2}+([\Delta^{\prime}]_{0}){{}_{|\overline{\Gamma_{1}}}})$)
$\displaystyle=(\Gamma_{1}+r\cdot\Delta+\Gamma_{2})+([\Delta^{\prime}]_{0}{{}_{|\Gamma_{1}}}+[\Delta^{\prime}]_{0}{{}_{|\overline{\Gamma_{1}}}})$
($\because$ $+$ associativity and commutativity)
$\displaystyle=(\Gamma_{1}+r\cdot\Delta+\Gamma_{2})+[\Delta^{\prime}]_{0}$
($\because$ Lemma 2)

Thus, we obtain the conclusion of the lemma.

  * •

Case (der)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime},y:B_{1}\vdash
t:B_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime},y:[B_{1}]_{1}\vdash
t:B_{2}\end{array}}$ (der)

In this case, we know
$(\Gamma^{\prime\prime},y:[B_{1}]_{1})=(\Gamma,x:[A]_{r},\Gamma^{\prime})$.
There are two cases in which the versioned assumption $x:[A]_{r}$ is
equivalent to $y:[B_{1}]_{1}$ and not equivalent to.

    * –

Suppose $x:[A]_{r}=y:[B_{1}]_{1}$
We know $x=y$, $A=B_{1}$, $r=1$, $\Gamma=\Gamma^{\prime\prime}$, and
$\Gamma^{\prime}=\emptyset$. The last derivation is rewritten as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime},x:A\vdash
t:B_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma^{\prime\prime},x:[A]_{1}\vdash
t:B_{2}\end{array}}$ (der)

We then apply Lemma 7 to the premise to obtain the following:

$\displaystyle\Gamma^{\prime\prime}+\Delta\vdash[t^{\prime}/x]t:B_{2}$

Note that $\Delta$ is a versioned assumption by the assumption 1 and thus
$\Gamma^{\prime\prime}+\Delta=\Gamma^{\prime\prime}+r\cdot\Delta$ where $r=1$,
we obtain the conclusion of the lemma.

    * –

Suppose $x:[A]_{r}\neq y:[B_{1}]_{1}$
Let $\Gamma_{1}$ and $\Gamma_{2}$ be typing contexts such that
$\Gamma^{\prime\prime}=(\Gamma_{1},x:[A]_{r},\Gamma_{1}^{\prime})$. The last
derivation is rewritten as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}(\Gamma_{1},x:[A]_{r},\Gamma_{1}^{\prime}),y:B_{1}\vdash
t:B_{2}\end{array}}{\begin{array}[]{@{}c@{}}(\Gamma_{1},x:[A]_{r},\Gamma_{1}^{\prime}),y:[B_{1}]_{1}\vdash
t:B_{2}\end{array}}$ (der)

We then apply the induction hypothesis to the premise of the last derivation
and reapply (der) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}(\Gamma+r\cdot\Delta+\Gamma^{\prime\prime}),y:B_{1}\vdash[t^{\prime}/x]t:B_{2}\end{array}}{\begin{array}[]{@{}c@{}}(\Gamma+r\cdot\Delta+\Gamma^{\prime\prime}),y:[B_{1}]_{1}\vdash[t^{\prime}/x]t:B_{2}\end{array}}$
(der)

Since $y:[B_{1}]_{1}$ is desjoint with
$\Gamma+r\cdot\Delta+\Gamma^{\prime\prime}$ and thus
$((\Gamma+r\cdot\Delta+\Gamma^{\prime\prime}),y:[B_{1}]_{1})=\Gamma+r\cdot\Delta+(\Gamma^{\prime\prime},y:[B_{1}]_{1})$,
we obtain the conclusion of the lemma.

  * •

Case (pr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{1}]\vdash t:B\quad\vdash
r^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}r^{\prime}\cdot[\Gamma_{1}]\vdash[t]:\Box_{r^{\prime}}B\end{array}}$
(pr)

Let $r^{\prime\prime}$ be a version resouce and $\Gamma^{\prime}_{1}$ and
$\Gamma^{\prime\prime}_{1}$ be typing contexts such that
$r^{\prime\prime}\sqsubseteq r^{\prime}$ and
$[\Gamma_{1}]=[\Gamma^{\prime}_{1},x:[A]_{r^{\prime\prime}},\Gamma^{\prime\prime}_{1}]$.
The last derivation is rewritten as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma^{\prime}_{1},x:[A]_{r^{\prime\prime}},\Gamma^{\prime\prime}_{1}]\vdash
t:B\end{array}}{\begin{array}[]{@{}c@{}}r^{\prime}\cdot[\Gamma^{\prime}_{1},x:[A]_{r^{\prime\prime}},\Gamma^{\prime\prime}_{1}]\vdash[t]:\Box_{r^{\prime}}B\end{array}}$
(pr)

We then compare the conclusion of the lemma and the above conclusion.

$\displaystyle(\Gamma,x:[A]_{r},\Gamma^{\prime})$
$\displaystyle=r^{\prime}\cdot[\Gamma_{1}]$
$\displaystyle=r^{\prime}\cdot[\Gamma^{\prime}_{1},x:[A]_{r^{\prime\prime}},\Gamma^{\prime\prime}_{1}]$
($\because$
$[\Gamma_{1}]=[\Gamma^{\prime}_{1},x:[A]_{r^{\prime\prime}},\Gamma^{\prime\prime}_{1}]$)
$\displaystyle=r^{\prime}\cdot[\Gamma^{\prime}_{1}],\
x:[A]_{r^{\prime\prime}\otimes r^{\prime}},\
r^{\prime}\cdot[\Gamma^{\prime\prime}_{1}]$ ($\because$ $\cdot$ definition)
$\displaystyle=r^{\prime}\cdot[\Gamma^{\prime}_{1}],\ x:[A]_{r^{\prime}},\
r^{\prime}\cdot[\Gamma^{\prime\prime}_{1}]$ ($\because$
$r^{\prime\prime}\sqsubseteq r^{\prime}$)

By the commutativity of ”,”, we can take $\Gamma$ and $\Gamma^{\prime}$
arbitrarily so that they satisfy the above equation. So here we know
$\Gamma=(r^{\prime}\cdot[\Gamma^{\prime}_{1}])$ and
$\Gamma^{\prime}=(r^{\prime}\cdot[\Gamma^{\prime\prime}_{1}])$.

We then apply the induction hypothesis to the premise of the last derivation
and reapply (pr) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma^{\prime}_{1}+r^{\prime\prime}\cdot\Delta+\Gamma^{\prime\prime}_{1}]\vdash[t^{\prime}/x]t:B\quad\vdash
r^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}r^{\prime}\cdot[\Gamma^{\prime}_{1}+r^{\prime\prime}\cdot\Delta+\Gamma^{\prime\prime}_{1}]\vdash[[t^{\prime}/x]t]:\Box_{r^{\prime}}B\end{array}}$
(pr)

where we use
$[\Gamma^{\prime}_{1},x:[A]_{r^{\prime\prime}},\Gamma^{\prime\prime}_{1}]=[\Gamma^{\prime}_{1}],x:[A]_{r^{\prime\prime}},[\Gamma^{\prime\prime}_{1}]$
and
$[\Gamma^{\prime}_{1}+r^{\prime\prime}\cdot\Delta+\Gamma^{\prime\prime}_{1}]=[\Gamma^{\prime}_{1}]+r^{\prime\prime}\cdot\Delta+[\Gamma^{\prime\prime}_{1}]$
before applying (pr).

Since $[[t^{\prime}/x]t]=[t^{\prime}/x][t]$ by the definiton of substitution,
the above conclusion is equivalent to the conclusion of the lemma except for
the typing contexts. Finally, we must show that
$(\Gamma+r^{\prime}\cdot\Delta+\Gamma^{\prime})=r^{\prime}\cdot[\Gamma^{\prime}_{1}+r^{\prime\prime}\cdot\Delta+\Gamma^{\prime\prime}_{1}]$
by the following reasoning:

$\displaystyle(\Gamma+r^{\prime}\cdot\Delta+\Gamma^{\prime})$
$\displaystyle=r^{\prime}\cdot[\Gamma^{\prime}_{1}]+r^{\prime}\cdot\Delta+r^{\prime}\cdot[\Gamma^{\prime}_{1}]$
($\because$ $\Gamma=(r^{\prime}\cdot[\Gamma^{\prime}_{1}])$ &
$\Gamma^{\prime}=(r^{\prime}\cdot[\Gamma^{\prime\prime}_{1}])$)
$\displaystyle=r^{\prime}\cdot[\Gamma^{\prime}_{1}]+(r^{\prime}\otimes
r^{\prime\prime})\cdot\Delta+r^{\prime}\cdot[\Gamma^{\prime}_{1}]$ ($\because$
$r^{\prime\prime}\sqsubseteq r^{\prime}$)
$\displaystyle=r^{\prime}\cdot[\Gamma^{\prime}_{1}]+r^{\prime}\cdot(r^{\prime\prime}\cdot\Delta)+r^{\prime}\cdot[\Gamma^{\prime}_{1}]$
($\because$ $\otimes$ associativity)
$\displaystyle=r^{\prime}\cdot[\Gamma^{\prime}_{1}+r^{\prime\prime}\cdot\Delta+\Gamma^{\prime}_{1}]$
($\because$ $\cdot$ distributive law over $+$)

Thus, we obtain the conclusion of the lemma.

  * •

Case (ver)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:B\quad\vdash\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}B\end{array}}$
(ver)

We compare the typing contexts between the lemma and the above conclusion as
follows:

$\displaystyle(\Gamma,x:[A]_{r},\Gamma^{\prime})$ $\displaystyle=\bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma_{i}]\right)$ $\displaystyle=\bigcup_{i\in
I_{x}}\ \left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i},\ x:[A]_{r_{i}},\
\Gamma^{\prime\prime}_{i}]\right)+\bigcup_{i\in J_{x}}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i},\
\Gamma^{\prime\prime}_{i}]\right)$ ($\because$
$I_{x}=\\{i\,|\,x\in\mathrm{dom}(\Gamma_{i})\\}$ and
$J_{x}=\\{i\,|\,x\notin\mathrm{dom}(\Gamma_{i})\\}$)

We then reorganise the typing context $\bigcup_{i\in I_{x}}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i},\ x:[A]_{r_{i}},\
\Gamma^{\prime\prime}_{i}]\right)$ as follows:

$\displaystyle\bigcup_{i\in I_{x}}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i},\ x:[A]_{r_{i}},\
\Gamma^{\prime\prime}_{i}]\right)$ $\displaystyle=$
$\displaystyle\bigcup_{i\in I_{x}}\ \left(\\{l_{i}\\}\cdot[x:[A]_{r_{i}},\
\Gamma^{\prime}_{i},\ \Gamma^{\prime\prime}_{i}]\right)$ ($\because$ ,
associativity) $\displaystyle=$ $\displaystyle\bigcup_{i\in I_{x}}\
\left(\\{l_{i}\\}\cdot(x:[A]_{r_{i}}),\
\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}],\
\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$ ($\because$ $\cdot$
distributive law) $\displaystyle=$ $\displaystyle\bigcup_{i\in I_{x}}\
\left(\\{l_{i}\\}\cdot(x:[A]_{r_{i}})\right),\ \bigcup_{i\in I_{x}}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}],\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$ Sum of each disjoint sub context) $\displaystyle=$
$\displaystyle\bigcup_{i\in I_{x}}\ \left(x:[A]_{\\{l_{i}\\}\otimes
r_{i}}\right),\ \bigcup_{i\in I_{x}}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}],\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$ $\cdot$ definition) $\displaystyle=$ $\displaystyle\
x:[A]_{\sum_{i\in I_{x}}\\{l_{i}\\}\otimes r_{i}},\ \ \bigcup_{i\in I_{x}}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}],\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$ $\bigcup$ and $+$ definition)

Thus, we obtain the following:

$\displaystyle(\Gamma,x:[A]_{r},\Gamma^{\prime})$ $\displaystyle=$
$\displaystyle\left(x:[A]_{\sum_{i\in I_{x}}\\{l_{i}\\}\otimes r_{i}},\ \
\bigcup_{i\in I_{x}}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}],\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)\right)+\bigcup_{i\in
J_{x}}\ \left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i},\
\Gamma^{\prime\prime}_{i}]\right)$ $\displaystyle=$ $\displaystyle\
x:[A]_{\sum_{i\in I_{x}}\\{l_{i}\\}\otimes r_{i}},\ \ \bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}],\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$ $\bigcup_{i\in J_{x}}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i},\
\Gamma^{\prime\prime}_{i}]\right)$ are disjoint with $x:[A]_{\sum_{i\in
I_{x}}\\{l_{i}\\}\otimes r_{i}}$)

Therefore, By Lemma 4, there exists typing contexts
$\Gamma^{\prime}_{\overline{i}}$ and $\Gamma^{\prime\prime}_{\overline{i}}$
such that:

$\displaystyle\Gamma^{\prime}_{\overline{i}},\Gamma^{\prime\prime}_{\overline{i}}$
$\displaystyle=\bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}],\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
$\displaystyle\Gamma^{\prime}_{\overline{i}}+\Gamma^{\prime\prime}_{\overline{i}}$
$\displaystyle=\bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]+\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$

Thus, we obtain the following:

$\displaystyle(\Gamma,x:[A]_{r},\Gamma^{\prime})$
$\displaystyle=x:[A]_{\sum_{i\in I_{x}}\\{l_{i}\\}\otimes r_{i}},\
\Gamma^{\prime}_{\overline{i}},\ \Gamma^{\prime\prime}_{\overline{i}}$
$\displaystyle=\Gamma^{\prime}_{\overline{i}},\ x:[A]_{\sum_{i\in
I_{x}}\\{l_{i}\\}\otimes r_{i}},\ \Gamma^{\prime\prime}_{\overline{i}}$
($\because$ , commutativity)

By the commutativity of ”,”, we can take $\Gamma$ and $\Gamma^{\prime}$
arbitrarily so that they satisfy the above equation. So here we know
$\Gamma=\Gamma^{\prime}_{\overline{i}}$,
$\Gamma^{\prime}=\Gamma^{\prime\prime}_{\overline{i}}$, and $r=\sum_{i\in
I_{x}}(\\{l_{i}\\}\otimes r_{i})$. We then apply the induction hypothesis to
the premise whose typing context contains $x$. Here, we define a typing
context $\Delta_{i}$ as follows:

$\displaystyle\Delta_{i}=\left\\{\begin{aligned} \Delta\hskip 10.00002pt(i\in
I_{x})\\\ \emptyset\hskip 10.00002pt(i\in J_{x})\\\ \end{aligned}\right.$

By using $\Delta_{i}$, we reapply (ver) as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma^{\prime}_{i}+r_{i}\cdot\Delta_{i}+\Gamma^{\prime\prime}_{i}]\vdash[t^{\prime}/x]t_{i}:B\quad\vdash\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}+r_{i}\cdot\Delta_{i}+\Gamma^{\prime\prime}_{i}])\vdash\\{\overline{l_{i}=[t^{\prime}/x]t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}B\end{array}}$
(ver)

Since
$\\{\overline{l_{i}=[t^{\prime}/x]t_{i}}\,|\,l_{k}\\}=[t^{\prime}/x]\\{\overline{l_{i}=t_{i}}\,|\,l_{k}\\}$
by the definition of substitution, the above conclusion is equivalent to the
conclusion of the lemma except for typing contexts. Finally, we must show that
$(\Gamma+r\cdot\Delta+\Gamma^{\prime})=\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}+r_{i}\cdot\Delta_{i}+\Gamma^{\prime\prime}_{i}])$.

$\displaystyle(\Gamma+r\cdot\Delta+\Gamma^{\prime})$
$\displaystyle=\Gamma^{\prime}_{\overline{i}}+r\cdot\Delta+\Gamma^{\prime\prime}_{\overline{i}}$
($\because$ $\Gamma=\Gamma^{\prime}_{\overline{i}}$ &
$\Gamma^{\prime}=\Gamma^{\prime\prime}_{\overline{i}}$)
$\displaystyle=r\cdot\Delta+(\Gamma^{\prime}_{\overline{i}}+\Gamma^{\prime\prime}_{\overline{i}})$
($+$ associativity & commutativity) $\displaystyle=r\cdot\Delta+\bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]+\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$
$\Gamma^{\prime}_{\overline{i}}+\Gamma^{\prime\prime}_{\overline{i}}=\bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]+\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$)
$\displaystyle=(\sum_{i\in I_{x}}(\\{l_{i}\\}\otimes
r_{i}))\cdot\Delta+\bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]+\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$ $r=\sum_{i\in I_{x}}(\\{l_{i}\\}\otimes r_{i})$)
$\displaystyle=\bigcup_{i\in
I_{x}}\left(\\{l_{i}\\}\cdot\left(r_{i}\cdot\Delta\right)\right)+\bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]+\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$ $\bigcup$ definition)
$\displaystyle=\bigcup_{i}\left(\\{l_{i}\\}\cdot\left(r_{i}\cdot\Delta_{i}\right)\right)+\bigcup_{i}\
\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]+\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$ $\Delta_{i}$ definition)
$\displaystyle=\bigcup_{i}\left(\\{l_{i}\\}\cdot\left(r_{i}\cdot\Delta_{i}\right)+\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]+\\{l_{i}\\}\cdot[\Gamma^{\prime\prime}_{i}]\right)$
($\because$ $+$ commutativity & associativity)
$\displaystyle=\bigcup_{i}\left(\\{l_{i}\\}\cdot\left(\left(r_{i}\cdot\Delta_{i}\right)+[\Gamma^{\prime}_{i}]+[\Gamma^{\prime\prime}_{i}]\right)\right)$
($\because$ districutive law)
$\displaystyle=\bigcup_{i}\left(\\{l_{i}\\}\cdot\left([\Gamma^{\prime}_{i}]+\left(r_{i}\cdot\Delta_{i}\right)+[\Gamma^{\prime\prime}_{i}]\right)\right)$
($\because$ $+$ commutativity)
$\displaystyle=\bigcup_{i}\left(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}+r_{i}\cdot\Delta_{i}+\Gamma^{\prime\prime}_{i}]\right)$
($\because$ $[\cdot]$ definition)

Thus, we obtain the conclusion of the lemma.

  * •

Case (veri)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:B\quad\vdash\\{\overline{l_{i}}\\}\quad
l_{k}\in\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle:B\end{array}}$
(veri)

This case is similar to the case of (ver).

  * •

Case (extr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash t:\Box_{r}A\quad l\in
r\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash t.l:A\end{array}}$ (extr)

In this case, we apply the induction hypothesis to the premise and then
reapply (extr), we obtain the conclusion of the lemma.

  * •

Case (sub)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2}\vdash
t:B\quad r_{1}\sqsubseteq r_{2}\quad\vdash
r_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2}\vdash
t:B\end{array}}$ (sub)

In this case, we know
$(\Gamma,x:[A]_{r},\Gamma^{\prime})=(\Gamma,y:[B^{\prime}]_{r_{2}},\Gamma^{\prime})$.
There are three cases where the versioned assumption $x:[A]_{r}$ is included
in $\Gamma_{1}$, included in $\Gamma_{2}$, or equal to
$y:[B^{\prime}]_{r_{2}}$.

    * –

Suppose $(x:[A]_{r})\in\Gamma_{1}$.
Let $\Gamma^{\prime}_{1}$ and $\Gamma^{\prime\prime}_{1}$ be typing contexts
such that
$\Gamma_{1}=(\Gamma^{\prime}_{1},x:[A]_{r},\Gamma^{\prime\prime}_{1})$. The
last derivation is rewritten as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma^{\prime}_{1},x:[A]_{r},\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2}\vdash
t:B\quad r_{1}\sqsubseteq r_{2}\quad\vdash
r_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma^{\prime}_{1},x:[A]_{r},\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2}\vdash
t:B\end{array}}$ (sub)

We then apply the induction hypothesis to the premise of the last derivation
to obtain the following:

$\displaystyle\Gamma^{\prime}_{1}+r\cdot\Delta+(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2})\vdash[t^{\prime}/x]t:B$
(1)

The typing context of the above conclusion can be transformed as follows:

$\displaystyle\Gamma^{\prime}_{1}+r\cdot\Delta+(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2})$
$\displaystyle=\ $
$\displaystyle(\Gamma^{\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime}_{1}}}),(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2}))}}},$
$\displaystyle\hskip
50.00008pt\left((\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2})+(r\cdot\Delta){{}_{|(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2})}}\right)$
($\because$ Lemma 6) $\displaystyle=\ $
$\displaystyle(\Gamma^{\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime}_{1}}}),(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2}))}}},$
$\displaystyle\hskip
50.00008pt\left((\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2})+\left((r\cdot\Delta){{}_{|\Gamma^{\prime\prime}_{1}}},(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{1}})}},(r\cdot\Delta){{}_{|\Gamma_{2}}})\right)\right)$
($\because$ 6) $\displaystyle=\ $
$\displaystyle(\Gamma^{\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime}_{1}}}),(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2}))}}},$
$\displaystyle\hskip
50.00008pt\left(\Gamma^{\prime\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime\prime}_{1}}}\right),\left(y:[B^{\prime}]_{r_{1}}+(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{1}})}}\right),\left(\Gamma_{2}+(r\cdot\Delta){{}_{|\Gamma_{2}}}\right)$
($\because$ Lemma 3) $\displaystyle=\ $
$\displaystyle\Gamma_{3},y:[B^{\prime}]_{r_{1}\oplus
r_{3}},\Gamma^{\prime}_{3}$

The last equational transformation holds by the following equation 2.

Let $\Gamma_{3}$ and $\Gamma^{\prime}_{3}$ be typing contexts that satisfy the
following:

$\displaystyle\Gamma_{3}$
$\displaystyle=(\Gamma^{\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime}_{1}}}),(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2}))}}},\left(\Gamma^{\prime\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime\prime}_{1}}}\right)$
$\displaystyle\Gamma^{\prime}_{3}$
$\displaystyle=\left(\Gamma_{2}+(r\cdot\Delta){{}_{|\Gamma_{2}}}\right)$

For $(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{1}})}}$, Let $r_{3}$ and
$r_{3}^{\prime}$ be typing contexts such that $r_{3}=r\otimes r^{\prime}_{3}$
and stisfy the following:

$\displaystyle(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{1}})}}=\left\\{\begin{aligned}
&r\cdot(y:[B^{\prime}]_{r^{\prime}_{3}})=y:[B^{\prime}]_{r\otimes
r^{\prime}_{3}}=y:[B^{\prime}]_{r_{3}}&(y\in\mathrm{dom}(\Delta))\\\
&\emptyset&(y\notin\mathrm{dom}(\Delta))\end{aligned}\right.$

Thus, we obtain the following equation.

$\displaystyle
y:[B^{\prime}]_{r_{1}}+(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{1}})}}=\left\\{\begin{aligned}
&y:[B^{\prime}]_{r_{1}\oplus r_{3}}&(y\in\mathrm{dom}(\Delta))\\\
&y:[B^{\prime}]_{r_{1}\oplus
r_{3}}=y:[B^{\prime}]_{r_{1}}&(y\notin\mathrm{dom}(\Delta))\end{aligned}\right.$
(2)

Applying all of the above transformations and reapplying (sub) to the
expression 1, we obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{3},y:[B^{\prime}]_{r_{1}\oplus
r_{3}},\Gamma^{\prime}_{3}\vdash[t^{\prime}/x]t:B\quad(r_{1}\oplus
r_{3})\sqsubseteq(r_{2}\oplus r_{3})\quad\vdash r_{2}\oplus
r_{3}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{3},y:[B^{\prime}]_{r_{2}\oplus
r_{3}},\Gamma^{\prime}_{3}\vdash[t^{\prime}/x]t:B\end{array}}$ (sub)

The conclusion of the above derivation is equivalent to the conclusion of the
lemma except for the typing contexts.

Finally, we must show that
$\Gamma^{\prime}_{1}+r\cdot\Delta+(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2})=(\Gamma_{3},y:[B^{\prime}]_{r_{2}\oplus
r_{3}},\Gamma^{\prime}_{3})$.

$\displaystyle\Gamma^{\prime}_{1}+r\cdot\Delta+(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2})$
$\displaystyle=\ $
$\displaystyle(\Gamma^{\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime}_{1}}}),(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2}))}}},$
$\displaystyle\hskip
50.00008pt\left((\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2})+(r\cdot\Delta){{}_{|(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2})}}\right)$
($\because$ Lemma 6) $\displaystyle=\ $
$\displaystyle(\Gamma^{\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime}_{1}}}),(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2}))}}},$
$\displaystyle\hskip
50.00008pt\left((\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2})+\left((r\cdot\Delta){{}_{|\Gamma^{\prime\prime}_{1}}},(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{2}})}},(r\cdot\Delta){{}_{|\Gamma_{2}}})\right)\right)$
($\because$ 6) $\displaystyle=\ $
$\displaystyle(\Gamma^{\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime}_{1}}}),(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2}))}}},$
$\displaystyle\hskip
50.00008pt\left(\Gamma^{\prime\prime}_{1}+(r\cdot\Delta){{}_{|\Gamma^{\prime\prime}_{1}}}\right),\left(y:[B^{\prime}]_{r_{2}}+(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{2}})}}\right),\left(\Gamma_{2}+(r\cdot\Delta){{}_{|\Gamma_{2}}}\right)$
($\because$ Lemma 3) $\displaystyle=\ $
$\displaystyle\Gamma_{3},y:[B^{\prime}]_{r_{2}\oplus
r_{3}},\Gamma^{\prime}_{3}$

The last transformation is based on the following equation that can be derived
from the definition 6.

$\displaystyle(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{1}},\Gamma_{2}))}}}$
$\displaystyle=(r\cdot\Delta){{}_{|\overline{(\Gamma^{\prime}_{1},(\Gamma^{\prime\prime}_{1},y:[B^{\prime}]_{r_{2}},\Gamma_{2}))}}}$
$\displaystyle(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{1}})}}$
$\displaystyle=(r\cdot\Delta){{}_{|(y:[B^{\prime}]_{r_{2}})}}$

Thus, we obtain the conclusion of the lemma.

    * –

Suppose $(x:[A]_{r})\in\Gamma_{2}$.
This case is similar to the case of $(x:[A]_{r})\in\Gamma_{1}$.

    * –

Suppose $(x:[A]_{r})=y:[B^{\prime}]_{r_{2}}$.
The last derivation is rewritten as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[A]_{r^{\prime}},\Gamma_{2}\vdash
t:B\quad r^{\prime}\sqsubseteq r\quad\vdash
r\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[A]_{r},\Gamma_{2}\vdash
t:B\end{array}}$ (sub)

We apply the induction hypothesis to the premise and then reapply (sub), we
obtain the conclusion of the lemma.

###  0.C.4 Type Safety

######  Lemma 9 (Inversion lemma)

Let $v$ be a value such that $\Gamma\vdash v:A$. The followings hold for a
type $A$.

  * •

$A=\textnormal{{Int}}\Longrightarrow$ $v=n$ for some integer constant $n$.

  * •

$A=\Box_{r}B\Longrightarrow$ $v=[t^{\prime}]$ for some term $t^{\prime}$, or
$v=\\{\overline{l_{i}=t_{i}}\\}$ for some terms $t_{i}$ and some labels
$l_{i}\in r$.

  * •

$A=B\rightarrow B^{\prime}\Longrightarrow$ $v=\lambda p.t$ for some pattern
$p$ and term $t$.

######  Lemma 10 (Type safety for default version overwriting)

For any version label $l$:

$\displaystyle\Gamma\vdash t:A\hskip 10.00002pt\Longrightarrow\hskip
10.00002pt\Gamma\vdash t@l:A$

###### Proof

The proof is given by induction on the typing derivation of $\Gamma\vdash
t:A$. Consider the cases for the last rule used in the typing derivation of
assumption.

  * •

Case (int)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash
n:\textsf{Int}\end{array}}$ (int)

This case holds trivially because $n@l\equiv n$ for any labels $l$.

  * •

Case (var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\vdash
A\end{array}}{\begin{array}[]{@{}c@{}}x:A\vdash x:A\end{array}}$ (var)

This case holds trivially because $x@l=x$ for any labels $l$.

  * •

Case (abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}-\vdash
p:B_{1}\rhd\Delta^{\prime}\quad\Gamma,\Delta^{\prime}\,\vdash\,t_{1}:A_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\,\vdash\,\lambda
p.t_{1}:A_{1}\rightarrow A_{2}\end{array}}$ (abs)

By induction hypothesis, there exists a term $t_{1}@l$ such that:

$\displaystyle\Gamma,\Delta^{\prime}\,\vdash\,t_{1}@l:A_{2}$

We then reapply (abs) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}-\vdash
p:B_{1}\rhd\Delta^{\prime}\quad\Gamma,\Delta^{\prime}\,\vdash\,t_{1}@l:A_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\,\vdash\,\lambda
p.(t_{1}@l):A_{1}\rightarrow A_{2}\end{array}}$ (abs)

Thus, note that $(\lambda p.t_{1})@l\equiv\lambda p.(t_{1}@l)$, we obtain the
conclusion of the lemma.

  * •

Case (app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t_{1}:B\rightarrow A\quad\Gamma_{2}\vdash
t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\vdash
t_{1}\,t_{2}:A\end{array}}$ (app)

By induction hypothesis, there exists terms $t_{1}@l$ and $t_{2}@l$ such that:

$\displaystyle\Gamma_{1}$ $\displaystyle\vdash t_{1}@l:B\rightarrow A$
$\displaystyle\Gamma_{2}$ $\displaystyle\vdash t_{2}@l:B$

We then reapply (app) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t_{1}@l:B\rightarrow A\quad\Gamma_{2}\vdash
t_{2}@l:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\vdash(t_{1}@l)\,(t_{2}@l):A\end{array}}$
(app)

Thus, note that $(t_{1}\,t_{2})@l\equiv(t_{1}@l)\,(t_{2}@l)$, we obtain the
conclusion of the lemma.

  * •

Case (let)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\,\vdash\,t_{1}:\Box_{r}A\quad\Gamma_{2},x:[A]_{r}\,\vdash\,t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\,\vdash\,\textbf{let
}[x]=t_{1}\textbf{ in }t_{2}:B\end{array}}$ (let)

By induction hypothesis, there exists terms $t_{1}@l$ and $2@l$ such that:

$\displaystyle\Gamma_{1}\,$ $\displaystyle\vdash\,t_{1}@l:\Box_{r}A$
$\displaystyle\Gamma_{2},x:[A]_{r}\,$ $\displaystyle\vdash\,t_{2}@l:B$

We then reapply (let) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\,\vdash\,t_{1}@l:\Box_{r}A\quad\Gamma_{2},x:[A]_{r}\,\vdash\,t_{2}@l:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\,\vdash\,\textbf{let
}[x]=(t_{1}@l)\textbf{ in }(t_{2}@l):B\end{array}}$ (let)

Thus, note that $(\textbf{let }[x]=t_{1}\textbf{ in }t_{2})@l\equiv\textbf{let
}[x]=(t_{1}@l)\textbf{ in }(t_{2}@l)$, we obtain the conclusion of the lemma.

  * •

Case (weak)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t:A\quad\vdash\Delta^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+[\Delta^{\prime}]_{0}\vdash
t:A\end{array}}$ (weak)

By induction hypothesis, we know the following:

$\displaystyle\Gamma_{1}\vdash t@l:A$

We then reapply (weak) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t@l:A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+[\Delta^{\prime}]_{0}\vdash
t@l:A\end{array}}$ (weak)

Thus, we obtain the conclusion of the lemma.

  * •

Case (der)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:B\vdash
t:A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{1}\vdash
t:A\end{array}}$ (der)

By induction hypothesis, there exists terms $t@l$ such that:

$\displaystyle\Gamma_{1},x:B\vdash t@l:A$

We then reapply (der) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:B\vdash
t@l:A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{1}\vdash
t@l:A\end{array}}$ (der)

Thus, we obtain the conclusion of the lemma.

  * •

Case (pr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma]\vdash t:B\quad\vdash
r\end{array}}{\begin{array}[]{@{}c@{}}r\cdot[\Gamma]\vdash[t]:\Box_{r}B\end{array}}$
(pr)

This case holds trivially because $[t]@l\equiv[t]$ for any labels $l$.

  * •

Case (ver)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:A\quad\vdash\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A\end{array}}$
(ver)

This case holds trivially because
$\\{\overline{l_{i}=t_{i}}\\}@l\equiv\\{\overline{l_{i}=t_{i}}\\}$ for any
labels $l$.

  * •

Case (veri)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:A\quad\vdash\\{\overline{l_{i}}\\}\quad
l_{k}\in\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle:A\end{array}}$
(veri)

In this case, there are two possibilities for the one step evaluation of $t$.

    * –

Suppose $l\in\\{\overline{l_{i}}\\}$.
We can apply the default version overwriting as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}l\in\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle@l\,\equiv\,\langle\overline{l_{i}=t_{i}}\,|\,l\rangle\end{array}}$

In this case, we can derive the type of
$\langle\overline{l_{i}=t_{i}}\,|\,l\rangle$ as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:A\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\langle\overline{l_{i}=t_{i}}\,|\,l\rangle:A\end{array}}$
(veri)

Thus, we obtain the conclusion of the lemma.

    * –

Suppose $l\notin\\{\overline{l_{i}}\\}$.
We can apply the default version overwriting as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}l\notin\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle@l\,\equiv\,\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle\end{array}}$

This case holds trivially because
$\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle@l=\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle$.

  * •

Case (extr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash t_{1}:\Box_{r}A\quad
l_{k}\in r\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
t_{1}.l_{k}:A\end{array}}$ (extr)

By induction hypothesis, there exists a term $t_{1}@l$ such that:

$\displaystyle\Gamma\vdash t_{1}@l:\Box_{r}A$

We then reapply (extr) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
t_{1}@l:\Box_{r}A\quad l_{k}\in
r\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash(t_{1}@l).l_{k}:A\end{array}}$
(extr)

Thus, note that $(t_{1}.l_{k})@l\equiv(t_{1}@l).l_{k}$, we obtain the
conclusion of the lemma.

  * •

Case (sub)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash
t:A\quad r\sqsubseteq s\quad\vdash
s\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{s},\Gamma_{2}\vdash
t:A\end{array}}$ (sub)

By induction hypothesis, there exists a term $t@l$ such that:

$\displaystyle\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash t@l:A$

We then reapply (sub) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash
t@l:A\quad r\sqsubseteq s\quad\vdash
s\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{s},\Gamma_{2}\vdash
t@l:A\end{array}}$ (sub)

Thus, we obtain the conclusion of the lemma.

######  Lemma 11 (Type-safe extraction for versioned values)

$\displaystyle[\Gamma]\vdash u:\Box_{r}A\hskip 10.00002pt\Longrightarrow\hskip
10.00002pt\forall l_{k}\in r.\ \exists t^{\prime}.\left\\{\begin{aligned}
&u.l_{k}\longrightarrow t^{\prime}&&\ (progress)\\\ &[\Gamma]\vdash
t^{\prime}:A&&\ (preservation)\end{aligned}\right.$

###### Proof

By inversion lemma (9), $u$ has either a form $[t^{\prime\prime}]$ or
$\\{\overline{l_{i}=t_{i}}\\}$.

  * •

Suppose $u=[t^{\prime\prime}]$.
We can apply (E-ex1) as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>t^{\prime\prime}@l_{k}\end{array}}$ (E-ex1)

Also, we get the following derivation for $v$.

$[\Gamma^{\prime}]\vdash t^{\prime\prime}:A$ $\vdash r$ (pr)
$r\cdot[\Gamma^{\prime}]\vdash[t^{\prime\prime}]:\Box_{r}A$ (weak) or (sub)
$\vdots$ (weak) or (sub) $[\Gamma]\vdash[t^{\prime\prime}]:\Box_{r}A$

By Lemma 10, we know the following:

$\displaystyle[\Gamma^{\prime}]\vdash t^{\prime\prime}@l_{k}:A$

Finally, we can rearrange the typing context as follows:

$[\Gamma^{\prime}]\vdash t^{\prime\prime}@l_{k}:A$ (weak) or (sub) $\vdots$
(weak) or (sub) $[\Gamma]\vdash t^{\prime\prime}@l_{k}:A$

Here, we follow the same manner as for the derivation of $[t^{\prime\prime}]$
(which may use (weak) and (sub)) to get $[\Gamma]$ from
$r\cdot[\Gamma^{\prime}]$.

Thus, we obtain the conclusion of the lemma.

  * •

Suppose $u=\\{\overline{l_{i}=t_{i}}\\}$.
We can apply (E-ex2) as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>t_{k}@l_{k}\end{array}}$ (E-ex2)

Also, we get the following derivation for $v$.

$[\Gamma^{\prime}_{i}]\vdash t_{i}:A$ $\vdash\\{\overline{l_{i}}\\}$ (ver)
$\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A$
(weak) or (sub) $\vdots$ (weak) or (sub)
$[\Gamma]\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A$

By Lemma 10, we know the following:

$\displaystyle[\Gamma^{\prime}_{k}]\vdash t_{k}@l_{k}:A$

Finally, we can rearrange the typing context as follows:

$[\Gamma^{\prime}_{k}]\vdash t_{k}@l_{k}:A$ $r_{kj}\sqsubseteq
r_{kj}\otimes\\{l_{k}\\}$ (sub) $*\,|\Gamma_{k}^{\prime}|$
$\underbrace{\\{l_{k}\\}\cdot[\Gamma^{\prime}_{k}]\vdash t_{k}@l_{k}:A}_{P}$

$P$
$r_{kj}\otimes\\{l_{k}\\}\sqsubseteq\textstyle{\sum_{i}}(r_{ij}\otimes\\{l_{i}\\})$
(sub) $*\,|\Gamma_{k}^{\prime}|$
$\textstyle{\bigcup_{i}}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])\vdash
t_{k}@l_{k}:A$ (weak) or (sub) $\vdots$ (weak) or (sub) $[\Gamma]\vdash
t_{k}@l_{k}:A$

Here in the multiple application of (sub), the second premise compares the
resources of j-th versioned assumption between the first premise and
conclusion. Also, we follow the same manner as for the derivation of
$\\{\overline{l_{i}=t_{i}}\\}$ (which may use (weak) and (sub)) to get
$[\Gamma]$ from
$\textstyle{\bigcup_{i}}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])$.

Thus, we obtain the conclusion of the lemma.

######  Theorem 0.C.1 (Type preservation for reductions)

$\displaystyle\left.\begin{aligned} &\Gamma\vdash t:A\\\ &t\leadsto
t^{\prime}\end{aligned}\right\\}\hskip 10.00002pt\Longrightarrow\hskip
10.00002pt\Gamma\vdash t^{\prime}:A$

###### Proof

The proof is given by induction on the typing derivation of $t$. Consider the
cases for the last rule used in the typing derivation of the first assumption.

  * •

Case (int)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash
n:\textsf{Int}\end{array}}$ (int)

This case holds trivially because there are no reduction rules that can be
applied to $n$.

  * •

Case (var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\vdash
A\end{array}}{\begin{array}[]{@{}c@{}}x:A\vdash x:A\end{array}}$ (var)

This case holds trivially because there are no reduction rules that can be
applied to $x$.

  * •

Case (abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}-\vdash
p:B_{1}\rhd\Delta^{\prime}\quad\Gamma,\Delta^{\prime}\,\vdash\,t_{1}:A_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\,\vdash\,\lambda
p.t_{1}:A_{1}\rightarrow A_{2}\end{array}}$ (abs)

This case holds trivially because there are no reduction rules that can be
applied to $\lambda p.t_{1}$.

  * •

Case (app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t_{1}:B\rightarrow A\quad\Gamma_{2}\vdash
t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\vdash
t_{1}\,t_{2}:A\end{array}}$ (app)

We perform case analysis for the ruduction rule applied last.

    * –

Case (E-abs1)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\underbrace{(\lambda
x.t^{\prime}_{1})\,t_{2}}_{t}\leadsto(t_{2}\rhd
x)\,t^{\prime}_{1}\end{array}}$ (E-abs1)

where $t_{1}=\lambda x.t^{\prime}_{1}$ for a term $t_{1}^{\prime}$. Then we
can apply ($\rhd_{\textrm{var}}$) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}(t_{2}\rhd
x)\,t^{\prime}_{1}=[t_{2}/x]t^{\prime}_{1}\end{array}}$
($\rhd_{\textrm{var}}$)

In this case, we know the typing derivation of $t$ has the following form:

$\Gamma^{\prime}_{1},x:B\vdash t^{\prime}_{1}:A$ (abs)
$\Gamma^{\prime}_{1}\vdash\lambda x.t^{\prime}_{1}:B\rightarrow A$ (weak),
(der), or (sub) $\vdots$ (weak), (der), or (sub) $\Gamma_{1}\vdash\lambda
x.t^{\prime}_{1}:B\rightarrow A$ $\Gamma_{2}\vdash t_{2}:B$ (app)
$\Gamma_{1}+\Gamma_{2}\vdash(\lambda x.t^{\prime}_{1})\,t_{2}:A$

By Lemma 7, we know the following:

$\displaystyle\left.\begin{aligned} \Gamma_{2}&\vdash t_{2}:B\\\
\Gamma^{\prime}_{1},x:B&\vdash t^{\prime}_{1}:A\end{aligned}\right\\}\hskip
10.00002pt\Longrightarrow\hskip
10.00002pt\Gamma^{\prime}_{1}+\Gamma_{2}\vdash[t_{2}/x]t^{\prime}_{1}:A$

Finally, we can rearrange the typing context as follows:

$\Gamma^{\prime}_{1}+\Gamma_{2}\vdash[t_{2}/x]t^{\prime}_{1}:A$ (weak), (der),
or (sub) $\vdots$ (weak), (der), or (sub)
$\Gamma_{1}+\Gamma_{2}\vdash[t_{2}/x]t^{\prime}_{1}:A$

Here, there exists a derive tree to get $\Gamma_{1}+\Gamma_{2}$ from
$\Gamma^{\prime}_{1}+\Gamma_{2}$ as for the derivation of $\lambda
x.t^{\prime}_{1}$ which may use (weak), (der) and (sub).

By choosing $t^{\prime}=[t_{2}/x]t^{\prime}_{1}$, we obtain the conclusion of
the theorem.

    * –

Case (E-abs2)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\underbrace{(\lambda[x].t^{\prime}_{1})\,t_{2}}_{t}\leadsto\underbrace{\textbf{let
}[x]=t_{2}\textbf{ in }t^{\prime}_{1}}_{t^{\prime}}\end{array}}$ (E-abs2)

In this case, we know the typing derivation of $t$ has the following form:

([pVar]) $r\vdash x:B\rhd x:[B]_{r}$ (p□) $-\vdash[x]:\Box_{r}B\rhd x:[B]_{r}$
$\Gamma_{1},x:[B]_{r}\vdash t_{1}^{\prime}:A$ (abs)
$\underbrace{\Gamma_{1}\vdash\lambda[x].t^{\prime}_{1}:\Box_{r}B\rightarrow
A}_{P}$

$P$ $\Gamma_{2}\vdash t_{2}:\Box_{r}B$ (app)
$\Gamma_{1}+\Gamma_{2}\vdash(\lambda[x].t^{\prime}_{1})\,t_{2}:A$

Therefore, we can construct the derivation tree for $t^{\prime}$ as follows.

$\Gamma_{2}\vdash t_{2}:\Box_{r}B$ $\Gamma_{1},x:[B]_{r}\vdash
t_{1}^{\prime}:A$ (app) $\Gamma_{1}+\Gamma_{2}\vdash\textbf{let
}[x]=t_{2}\textbf{ in }t^{\prime}_{1}:A$

Hence, we have the conclusion of the theorem.

  * •

Case (let)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\,\vdash\,t_{1}:\Box_{r}A\quad\Gamma_{2},x:[A]_{r}\,\vdash\,t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\,\vdash\,\textbf{let
}[x]=t_{1}\textbf{ in }t_{2}:B\end{array}}$ (let)

The only reduction rule we can apply is (E-clet) with two substitution rules,
depending on whether $t_{1}$ has the form $[t^{\prime}_{1}]$ or
$\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}$.

    * –

Suppose $t_{1}=[t_{1}^{\prime}]$.
We can apply (E-clet) to obtain the following.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\underbrace{\textbf{let
}[x]=[t_{1}^{\prime}]\textbf{ in
}t_{2}}_{t}\leadsto([t_{1}^{\prime}]\rhd[x])t_{2}\end{array}}$ (E-clet)

Thus, we can apply ($\rhd_{\square}$) and ($\rhd_{\textnormal{var}}$) to
obtain the following.

($\rhd_{\textnormal{var}}$) $(t_{1}^{\prime}\rhd
x)t_{2}=[t_{1}^{\prime}/x]t_{2}$ ($\rhd_{\square}$)
$([t_{1}^{\prime}]\rhd[x])t_{2}=[t_{1}^{\prime}/x]t_{2}$

In this case, we know the typing derivation of $t$ has the following form:

$[\Gamma_{1}^{\prime}]\vdash t^{\prime}_{1}:A$ $\vdash r$ (pr)
$r\cdot[\Gamma_{1}^{\prime}]\,\vdash\,[t_{1}^{\prime}]:\Box_{r}A$ (weak) or
(sub) $\vdots$ (weak) or (sub)
$\Gamma_{1}\,\vdash\,[t_{1}^{\prime}]:\Box_{r}A$
$\Gamma_{2},x:[A]_{r}\,\vdash\,t_{2}:B$ (let)
$\Gamma_{1}+\Gamma_{2}\,\vdash\,\textbf{let }[x]=[t_{1}^{\prime}]\textbf{ in
}t_{2}:B$

By Lemma 8, we know the following:

$\displaystyle\left.\begin{aligned}
[\Gamma_{1}^{\prime}]&\,\vdash\,t^{\prime}_{1}:A\\\
\Gamma_{2},x:[A]_{r}&\,\vdash\,t_{2}:B\end{aligned}\right\\}\hskip
10.00002pt\Longrightarrow\hskip
10.00002pt\Gamma_{2}+r\cdot[\Gamma_{1}^{\prime}]\,\vdash\,[t^{\prime}_{1}/x]t_{2}:B$

Finally, we can rearrange the typing context as follows:

$\Gamma_{2}+r\cdot[\Gamma_{1}^{\prime}]\,\vdash\,[t^{\prime}_{1}/x]t_{2}:B$
(weak) or (sub) $\vdots$ (weak) or (sub)
$\Gamma_{2}+\Gamma_{1}\,\vdash\,[t^{\prime}_{1}/x]t_{2}:B$

Here, there exists a derive tree to get $\Gamma_{2}+\Gamma_{1}$ from
$\Gamma_{2}+r\cdot[\Gamma_{1}^{\prime}]$ as for the derivation of
$[t^{\prime}_{1}]$ which may use (weak) and (sub).

Thus, by choosing $t^{\prime}=[t^{\prime}_{1}/x]t_{2}$, we obtain the
conclusion of the theorem.

    * –

Suppose $t_{1}=\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}$.
We can apply (E-clet) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\underbrace{\textbf{let
}[x]=\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}\textbf{ in
}t_{2}}_{t}\leadsto(\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}\rhd[x])t_{2}\end{array}}$
(E-clet)

Thus, we can apply ($\rhd_{\textnormal{ver}}$) and ($\rhd_{\textnormal{var}}$)
to obtain the following.

($\rhd_{\textnormal{var}}$)
$(\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle\rhd
x)t_{2}=[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}$
($\rhd_{\textnormal{ver}}$)
$(\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}\rhd[x])t_{2}=[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}$

In this case, we know the typing derivation of $t$ has the following form:

$[\Gamma_{i}^{\prime}]\vdash t^{\prime\prime}_{i}:A$
$\vdash\\{\overline{l_{i}}\\}$ (ver)
$\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])\,\vdash\,\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A$
(weak) or (sub) $\vdots$ (weak) or (sub)
$\underbrace{\Gamma_{1}\,\vdash\,\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A}_{P}$

$P$ $\Gamma_{2},x:A\,\vdash\,t_{2}:B$ (der)
$\Gamma_{2},x:[A]_{1}\,\vdash\,t_{2}:B$ (sub)$*|\\{\overline{l_{i}}\\}|$
$\Gamma_{2},x:[A]_{\\{\overline{l_{i}}\\}}\,\vdash\,t_{2}:B$ (let)
$\Gamma_{1}+\Gamma_{2}\,\vdash\,\textbf{let
}[x]=\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}\textbf{ in }t_{2}:B$

Then we can derive the type of
$\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle$ as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma^{\prime}_{i}]\,\vdash\,t^{\prime\prime}_{i}:A\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])\,\vdash\,\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle:A\end{array}}$
(veri)

By Lemma 7, we know the following:

$\displaystyle\left.\begin{aligned}
\textstyle{\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])}&\vdash\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle:A\\\
\Gamma_{2},x:A&\vdash t_{2}:B\end{aligned}\right\\}\hskip
1.00006pt\Longrightarrow\hskip 1.00006pt\left.\begin{aligned}
\Gamma_{2}+&\textstyle{\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])}\\\
&\,\vdash\,[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}:B\end{aligned}\right.$

Finally, we can rearrange the typing context as follows:

$\Gamma_{2}+\textstyle{\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])}\,\vdash\,[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}:B$
(weak) or (sub) $\vdots$ (weak) or (sub)
$\Gamma_{2}+\Gamma_{1}\,\vdash\,[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}:B$

Here, there exists a derive tree to get $\Gamma_{2}+\Gamma_{1}$ from
$\Gamma_{2}+\textstyle{\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}])}$ as
for the derivation of $\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}$ which may
use (weak) and (sub).

Thus, by choosing
$t^{\prime}=[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}$,
we obtain the conclusion of the theorem.

  * •

Case (weak)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t:A\quad\vdash\Delta^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+[\Delta^{\prime}]_{0}\vdash
t:A\end{array}}$ (weak)

In this case, $t$ does not change between before and after the last
derivation. The induction hypothesis implies that there exists a term
$t^{\prime\prime}$ such that:

$\displaystyle t\leadsto t^{\prime\prime}\ \land\ \Gamma_{1}\vdash
t^{\prime\prime}:A$ (ih)

We then reapply (weak) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t^{\prime\prime}:A\quad\vdash\Delta^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+[\Delta^{\prime}]_{0}\vdash
t^{\prime\prime}:A\end{array}}$ (weak)

Thus, by choosing $t^{\prime}=t^{\prime\prime}$, we obtain the conclusion of
the theorem.

  * •

Case (der)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:B\vdash
t:A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{1}\vdash
t:A\end{array}}$ (der)

In this case, $t$ does not change between before and after the last
derivation. The induction hypothesis implies that there exists a term
$t^{\prime\prime}$ such that:

$\displaystyle t\leadsto t^{\prime\prime}\ \land\ \Gamma_{1},x:B\vdash
t^{\prime\prime}:A$ (ih)

We then reapply (der) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:B\vdash
t^{\prime\prime}:A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{1}\vdash
t^{\prime\prime}:A\end{array}}$ (der)

Thus, by choosing $t^{\prime}=t^{\prime\prime}$, we obtain the conclusion of
the theorem.

  * •

Case (pr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma]\vdash
t^{\prime\prime}:B\quad\vdash
r\end{array}}{\begin{array}[]{@{}c@{}}r\cdot[\Gamma]\vdash[t^{\prime\prime}]:\Box_{r}B\end{array}}$
(pr)

This case holds trivially because there are no reduction rules that can be
applied to $[t^{\prime\prime}]$.

  * •

Case (ver)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:A\quad\vdash\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A\end{array}}$
(ver)

This case holds trivially because there are no reduction rules that can be
applied to $\\{\overline{l_{i}=t_{i}}\\}$.

  * •

Case (veri)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:A\quad\vdash\\{\overline{l_{i}}\\}\quad
l_{k}\in\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle:A\end{array}}$
(veri)

In this case, the only reduction rule we can apply is (E-veri).

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\underbrace{\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle}_{t}\leadsto
t_{k}@l_{k}\end{array}}$ (E-veri)

By Lemma 10, we obtain the following:

$\displaystyle[\Gamma_{k}]\vdash t_{k}:A\hskip 10.00002pt\Longrightarrow\hskip
10.00002pt[\Gamma_{k}]\vdash t_{k}@l_{k}:A$

Finally, we can rearrange the typing context as follows:

$[\Gamma_{k}]\vdash t_{k}@l_{k}:A$ (weak), (der) or (sub) $\vdots$ (weak),
(der) or (sub) $\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash t_{k}@l_{k}:A$

Thus, by choosing $t^{\prime}=t_{k}@l_{k}$, we obtain the conclusion of the
theorem.

  * •

Case (extr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash t_{1}:\Box_{r}A\quad
l_{k}\in r\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
t_{1}.l_{k}:A\end{array}}$ (extr)

In this case, there are two reduction rules that we can apply to $t$,
dependenig on whether $t_{1}$ has the form $[t^{\prime}_{1}]$ or
$\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}$.

    * –

Suppose $t_{1}=[t^{\prime}_{1}]$.
We know the typing derivation of $t$ has the following form:

$[\Gamma^{\prime}]\vdash t^{\prime}_{1}:A$ $\vdash r$ (pr)
$r\cdot[\Gamma^{\prime}]\vdash[t^{\prime}_{1}]:\Box_{r}A$ (weak) or (sub)
$\vdots$ (weak) or (sub) $\Gamma\vdash[t^{\prime}_{1}]:\Box_{r}A$ $l_{k}\in r$
(extr) $\Gamma\vdash[t^{\prime}_{1}].l_{k}:A$

By Lemma 11, we know the following:

$\displaystyle r\cdot[\Gamma^{\prime}]\vdash[t^{\prime}_{1}]:\Box_{r}A\hskip
10.00002pt\Longrightarrow\hskip 10.00002pt\exists
t^{\prime}.\left\\{\begin{aligned} &[t^{\prime}_{1}].l_{k}\longrightarrow
t^{\prime}\\\ &r\cdot[\Gamma^{\prime}]\vdash t^{\prime}:A\end{aligned}\right.$

Finally, we can rearrange the typing context as follows:

$r\cdot[\Gamma^{\prime}]\vdash t^{\prime}:A$ (weak) or (sub) $\vdots$ (weak)
or (sub) $\Gamma\vdash t^{\prime}:A$

Here, we follow the same manner as for the derivation of $[t^{\prime}_{1}]$
(which may use (weak) and (sub)) to get $\Gamma$ from
$r\cdot[\Gamma^{\prime}]$.

Thus, we obtain the conclusion of the theorem.

    * –

Suppose $t_{1}=\\{\overline{l_{i}=t_{i}}\\}$.
The last derivation is rewritten as follows:

$[\Gamma^{\prime}_{i}]\vdash t_{i}:A$ $\vdash\\{\overline{l_{i}}\\}$ (ver)
$\bigcup_{i}\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A$
(weak) or (sub) $\vdots$ (weak) or (sub)
$\Gamma\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A$
$l_{k}\in\\{\overline{l_{i}}\\}$ (extr)
$\Gamma\vdash\\{\overline{l_{i}=t_{i}}\\}.l_{k}:A$

By Lemma 11, we know the following:

$\displaystyle\textstyle{\bigcup_{i}}\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A\hskip
10.00002pt\Longrightarrow\hskip 10.00002pt\exists
t^{\prime}.\left\\{\begin{aligned}
&\\{\overline{l_{i}=t_{i}}\\}.l_{k}\longrightarrow t^{\prime}\\\
&\textstyle{\bigcup_{i}}\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]\vdash
t^{\prime}:A\end{aligned}\right.$

Finally, we can rearrange the typing context as follows:

$\textstyle{\bigcup_{i}}\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]\vdash
t^{\prime}:A$ (weak) or (sub) $\vdots$ (weak) or (sub) $\Gamma\vdash
t^{\prime}:A$

Here, we follow the same manner as for the derivation of
$\\{\overline{l_{i}=t_{i}}\\}$ (which may use (weak) and (sub)) to get
$\Gamma$ from $\bigcup_{i}\\{l_{i}\\}\cdot[\Gamma^{\prime}_{i}]$.

Thus, we obtain the conclusion of the theorem.

  * •

Case (sub)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash
t:A\quad r\sqsubseteq s\quad\vdash
s\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{s},\Gamma_{2}\vdash
t:A\end{array}}$ (sub)

In this case, $t$ does not change between before and after the last
derivation. The induction hypothesis implies that there exists a term
$t^{\prime\prime}$ such that:

$\displaystyle t\leadsto t^{\prime\prime}\ \land\
\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash t^{\prime\prime}:A$ (ih)

We then reapply (sub) to obtain the following:

$\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash t^{\prime\prime}:A$ $r\sqsubseteq s$
$\vdash s$ (sub) $\Gamma_{1},x:[B]_{s},\Gamma_{2}\vdash t^{\prime\prime}:A$

Thus, by choosing $t^{\prime}=t^{\prime\prime}$, we obtain the conclusion of
the theorem.

######  Theorem 0.C.2 (Type preservation for evaluations)

$\displaystyle\left.\begin{aligned} &\Gamma\vdash t:A\\\ &t\longrightarrow
t^{\prime}\end{aligned}\right\\}\hskip 10.00002pt\Longrightarrow\hskip
10.00002pt\Gamma\vdash t^{\prime}:A$

###### Proof

The proof is given by induction on the typing derivation of $t$. Consider the
cases for the last rule used in the typing derivation of the first assumption.

  * •

Case (int)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash
n:\textsf{Int}\end{array}}$ (int)

This case holds trivially because there are no evaluation rules that can be
applied to $n$.

  * •

Case (var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\vdash
A\end{array}}{\begin{array}[]{@{}c@{}}x:A\vdash x:A\end{array}}$ (var)

This case holds trivially because there are no evaluation rules that can be
applied to $x$.

  * •

Case (abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}-\vdash
p:B_{1}\rhd\Delta^{\prime}\quad\Gamma,\Delta^{\prime}\,\vdash\,t_{1}:A_{2}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\,\vdash\,\lambda
p.t_{1}:A_{1}\rightarrow A_{2}\end{array}}$ (abs)

This case holds trivially because there are no evaluation rules that can be
applied to $\lambda p.t_{1}$.

  * •

Case (app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t_{1}:B\rightarrow A\quad\Gamma_{2}\vdash
t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\vdash
t_{1}\,t_{2}:A\end{array}}$ (app)

In this case, there are two evaluation rules that can be applied to $t$.

    * –

Suppose the evaluation rule matches to $[\cdot].$
We perform the case analysis for the last ruduction rule.

      * *

Case (E-abs1) We know the evaluation of the assumption has the following form:

E-abs1 $(\lambda x.t^{\prime}_{1})\,t_{2}\leadsto(t_{2}\rhd
x)\,t^{\prime}_{1}$ $\underbrace{(\lambda
x.t^{\prime}_{1})\,t_{2}}_{t}\longrightarrow\underbrace{(t_{2}\rhd
x)\,t^{\prime}_{1}}_{t^{\prime}}$

By Lemma 0.C.1, we know the following:

$\displaystyle\left.\begin{aligned} &\Gamma_{1}+\Gamma_{2}\vdash(\lambda
x.t^{\prime}_{1})\,t_{2}:A\\\ &(\lambda
x.t^{\prime}_{1})\,t_{2}\leadsto(t_{2}\rhd
x)\,t^{\prime}_{1}\end{aligned}\right\\}\hskip 10.00002pt\Longrightarrow\hskip
10.00002pt\Gamma_{1}+\Gamma_{2}\vdash(t_{2}\rhd x)\,t^{\prime}_{1}:A$

Thus, we obtain the conclusion of the theorem.

      * *

Case (E-abs2)

E-abs2 $(\lambda[x].t^{\prime}_{1})\,t_{2}\leadsto\textbf{let
}[x]=t_{2}\textbf{ in }t_{1}^{\prime}$
$\underbrace{(\lambda[x].t^{\prime}_{1})\,t_{2}}_{t}\longrightarrow\underbrace{\textbf{let
}[x]=t_{2}\textbf{ in }t_{1}^{\prime}}_{t^{\prime}}$

In this case, we know the typing derivation of $t$ has the following form:

([pVar]) $r\vdash x:B\rhd x:[B]_{r}$ (p□) $-\vdash[x]:\Box_{r}B\rhd x:[B]_{r}$
$\Gamma_{1},x:[B]_{r}\vdash t_{1}^{\prime}:A$ (abs)
$\underbrace{\Gamma_{1}\vdash\lambda[x].t^{\prime}_{1}:\Box_{r}B\rightarrow
A}_{P}$

$P$ $\Gamma_{2}\vdash t_{2}:\Box_{r}B$ (app)
$\Gamma_{1}+\Gamma_{2}\vdash(\lambda[x].t^{\prime}_{1})\,t_{2}:A$

Therefore, we can construct the derivation tree for $t^{\prime}$ as follows.

$\Gamma_{2}\vdash t_{2}:\Box_{r}B$ $\Gamma_{1},x:[B]_{r}\vdash
t_{1}^{\prime}:A$ (app) $\Gamma_{1}+\Gamma_{2}\vdash\textbf{let
}[x]=t_{2}\textbf{ in }t^{\prime}_{1}:A$

Hence, we have the conclusion of the theorem.

    * –

Suppose the evaluation rule matches to $E\,t$.
We know the evaluation of the assumption has the following form:

$t^{\prime}_{1}\leadsto t^{\prime\prime}_{1}$
$\underbrace{E[t^{\prime}_{1}]\,t_{2}}_{t}\longrightarrow
E[t^{\prime\prime}_{1}]\,t_{2}$

where $t_{1}=E[t^{\prime}_{1}]$.

By induction hypothesis, we know the following:

$\displaystyle\left.\begin{aligned} &\Gamma_{1}\vdash
E[t^{\prime}_{1}]:B\rightarrow A\\\ &E[t^{\prime}_{1}]\longrightarrow
E[t^{\prime\prime}_{1}]\end{aligned}\right\\}\hskip
10.00002pt\Longrightarrow\hskip 10.00002pt\Gamma_{1}\vdash
E[t^{\prime\prime}_{1}]:B\rightarrow A$ (ih)

We then reapply (app) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
E[t^{\prime\prime}_{1}]:B\rightarrow A\quad\Gamma_{2}\vdash
t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\vdash
E[t^{\prime\prime}_{1}]\,t_{2}:A\end{array}}$ (app)

Thus, we obtain the conclusion of the theorem.

  * •

Case (let)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\,\vdash\,t_{1}:\Box_{r}A\quad\Gamma_{2},x:[A]_{r}\,\vdash\,t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\,\vdash\,\textbf{let
}[x]=t_{1}\textbf{ in }t_{2}:B\end{array}}$ (let)

In this case, there are two evaluation rules that we can apply to $t$.

    * –

Suppose the evaluation rule matches to $[\cdot]$.
We know the evaluation of the assumption has the following form:

(E-clet) $\textbf{let }[x]=[t_{1}^{\prime}]\textbf{ in
}t_{2}\leadsto([t_{1}^{\prime}]\rhd[x])t_{2}$ $\underbrace{\textbf{let
}[x]=[t_{1}^{\prime}]\textbf{ in
}t_{2}}_{t}\longrightarrow([t_{1}^{\prime}]\rhd[x])t_{2}$

By Lemma 0.C.1, we know the following:

$\displaystyle\left.\begin{aligned} &\Gamma_{1}+\Gamma_{2}\vdash\textbf{let
}[x]=[t_{1}^{\prime}]\textbf{ in }t_{2}:B\\\ &\textbf{let
}[x]=[t_{1}^{\prime}]\textbf{ in
}t_{2}\leadsto([t_{1}^{\prime}]\rhd[x])t_{2}\end{aligned}\right\\}\hskip
10.00002pt\Longrightarrow\hskip
10.00002pt\Gamma_{1}+\Gamma_{2}\vdash([t_{1}^{\prime}]\rhd[x])t_{2}:B$

Thus, we obtain the conclusion of the theorem.

    * –

Suppose the evaluation rule matches to $\textbf{let }[x]=E\textbf{ in }t$.
We know the evaluation of the assumption has the following form:

$t^{\prime}_{1}\leadsto t^{\prime\prime}_{1}$ $\underbrace{\textbf{let
}[x]=E[t^{\prime}_{1}]\textbf{ in }t_{2}}_{t}\longrightarrow\textbf{let
}[x]=E[t^{\prime\prime}_{1}]\textbf{ in }t_{2}$

where $t_{1}=E[t^{\prime}_{1}]$.

By induction hypothesis, we know the following:

$\displaystyle\left.\begin{aligned} &\Gamma_{1}\vdash
E[t^{\prime}_{1}]:\Box_{r}A\\\ &E[t^{\prime}_{1}]\longrightarrow
E[t^{\prime\prime}_{1}]\end{aligned}\right\\}\hskip
10.00002pt\Longrightarrow\hskip 10.00002pt\Gamma_{1}\vdash
E[t^{\prime\prime}_{1}]:\Box_{r}A$ (ih)

We then reapply (let) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\,\vdash\,E[t^{\prime\prime}_{1}]:\Box_{r}A\quad\Gamma_{2},x:[A]_{r}\,\vdash\,t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+\Gamma_{2}\,\vdash\,\textbf{let
}[x]=E[t^{\prime\prime}_{1}]\textbf{ in }t_{2}:B\end{array}}$ (let)

Thus, we obtain the conclusion of the theorem.

  * •

Case (weak)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t:A\quad\vdash\Delta^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+[\Delta^{\prime}]_{0}\vdash
t:A\end{array}}$ (weak)

In this case, $t$ does not change between before and after the last
derivation. The induction hypothesis implies that there exists a term
$t^{\prime}$ such that:

$\displaystyle t\longrightarrow t^{\prime}\ \land\ \Gamma_{1}\vdash
t^{\prime}:A$ (ih)

We then reapply (weak) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1}\vdash
t^{\prime}:A\quad\vdash\Delta^{\prime}\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1}+[\Delta^{\prime}]_{0}\vdash
t^{\prime}:A\end{array}}$ (weak)

Thus, we obtain the conclusion of the theorem.

  * •

Case (der)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:B\vdash
t:A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{1}\vdash
t:A\end{array}}$ (der)

In this case, $t$ does not change between before and after the last
derivation. The induction hypothesis implies that there exists a term
$t^{\prime}$ such that:

$\displaystyle t\longrightarrow t^{\prime}\ \land\ \Gamma_{1},x:B\vdash
t^{\prime}:A$ (ih)

We then reapply (der) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:B\vdash
t^{\prime}:A\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{1}\vdash
t^{\prime}:A\end{array}}$ (der)

Thus, we obtain the conclusion of the theorem.

  * •

Case (pr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma]\vdash
t^{\prime\prime}:B\quad\vdash
r\end{array}}{\begin{array}[]{@{}c@{}}r\cdot[\Gamma]\vdash[t^{\prime\prime}]:\Box_{r}B\end{array}}$
(pr)

This case holds trivially because there are no evaluation rules that can be
applied to $[t^{\prime\prime}]$.

  * •

Case (ver)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:A\quad\vdash\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A\end{array}}$
(ver)

This case holds trivially because there are no evaluation rules that can be
applied to $\\{\overline{l_{i}=t_{i}}\\}$.

  * •

Case (veri)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}[\Gamma_{i}]\vdash
t_{i}:A\quad\vdash\\{\overline{l_{i}}\\}\quad
l_{k}\in\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\bigcup_{i}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle:A\end{array}}$
(veri)

In this case, the only evaluation rule we can apply is evaluation for
$[\cdot]$. We know the evaluation of the assumption has the following form:

E-veri $\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle\leadsto t_{k}@l_{k}$
$\underbrace{\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle}_{t}\longrightarrow
t_{k}@l_{k}$

By Lemma 0.C.1, we know the following:

$\displaystyle\left.\begin{aligned}
&\textstyle{\bigcup_{i}}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle:A\\\
&\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle\leadsto
t_{k}@l_{k}\end{aligned}\right\\}\hskip 10.00002pt\Longrightarrow\hskip
10.00002pt\textstyle{\bigcup_{i}}(\\{l_{i}\\}\cdot[\Gamma_{i}])\vdash
t_{k}@l_{k}:A$

Thus, we obtain the conclusion of the theorem.

  * •

Case (extr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash t_{1}:\Box_{r}A\quad
l_{k}\in r\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
t_{1}.l_{k}:A\end{array}}$ (extr)

In this case, there are two evaluation rules that we can apply to $t$.

    * –

Suppose the evaluation rule matches to $[\cdot]$.
We know the evaluation of the assumption has the following form:

E-ex1 or E-ex2 $t_{1}.l_{k}\leadsto t^{\prime}_{1}$
$\underbrace{t_{1}.l_{k}}_{t}\longrightarrow t^{\prime}_{1}$

By Lemma 0.C.1, we know the following:

$\displaystyle\left.\begin{aligned} &\Gamma\vdash t_{1}.l_{k}:A\\\
&t_{1}.l_{k}\leadsto t^{\prime}_{1}\end{aligned}\right\\}\hskip
10.00002pt\Longrightarrow\hskip 10.00002pt\Gamma\vdash t^{\prime}_{1}:A$

Thus, we obtain the conclusion of the theorem.

    * –

Suppose the evaluation rule matches to $E.l$.
We know the evaluation of the assumption has the following form:

$t^{\prime}_{1}\leadsto t^{\prime\prime}_{1}$
$\underbrace{E[t^{\prime}_{1}].l_{k}}_{t}\longrightarrow
E[t^{\prime\prime}_{1}].l_{k}$

where $t_{1}=E[t^{\prime}_{1}]$.

By induction hypothesis, we know the following:

$\displaystyle\left.\begin{aligned} &\Gamma\vdash
E[t^{\prime}_{1}]:\Box_{r}A\\\ &E[t^{\prime}_{1}]\longrightarrow
E[t^{\prime\prime}_{1}]\end{aligned}\right\\}\hskip
10.00002pt\Longrightarrow\hskip 10.00002pt\Gamma\vdash
E[t^{\prime\prime}_{1}]:\Box_{r}A$ (ih)

We the reapply (extr) to obtain the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma\vdash
E[t^{\prime\prime}_{1}]:\Box_{r}A\quad l_{k}\in
r\end{array}}{\begin{array}[]{@{}c@{}}\Gamma\vdash
E[t^{\prime\prime}_{1}].l_{k}:A\end{array}}$ (extr)

Thus, we obtain the conclusion of the theorem.

  * •

Case (sub)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash
t:A\quad r\sqsubseteq s\quad\vdash
s\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{s},\Gamma_{2}\vdash
t:A\end{array}}$ (sub)

In this case, $t$ does not change between before and after the last
derivation. The induction hypothesis implies that there exists a term
$t^{\prime}$ such that:

$\displaystyle t\longrightarrow t^{\prime}\ \land\
\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash t^{\prime}:A$ (ih)

We then reapply (sub) to obtain the following:

$\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash t^{\prime}:A$ $r\sqsubseteq s$ $\vdash
s$ (sub) $\Gamma_{1},x:[B]_{s},\Gamma_{2}\vdash t^{\prime}:A$

Thus, we obtain the conclusion of the theorem.

######  Theorem 0.C.3 ($\lambda_{\mathrm{VL}}$ progress)

$\displaystyle\emptyset\vdash t:A\Longrightarrow(\textnormal{{value}}\
t)\lor(\exists t^{\prime}.t\longrightarrow t^{\prime})$

###### Proof

The proof is given by induction on the typing derivation of $t$. Consider the
cases for the last rule used in the typing derivation of the assumption.

  * •

Case (int)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash
n:\textsf{Int}\end{array}}$ (int)

This case holds trivially because value $n$.

  * •

Case (var) This case holds trivially because $x:A$ cannot be $\emptyset$.

  * •

Case (abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}-\vdash
p:A_{1}\rhd\Delta^{\prime}\quad\Delta^{\prime}\,\vdash\,t:A_{2}\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\,\vdash\,\lambda
p.t:A_{1}\rightarrow A_{2}\end{array}}$ (abs)

This case holds trivially because value $\lambda p.t$.

  * •

Case (app)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\emptyset\vdash t_{1}:B\rightarrow
A\quad\emptyset\vdash
t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash
t_{1}\,t_{2}:A\end{array}}$ (app)

There are two cases whether $t_{1}$ is a value or not.

    * –

Suppose $t_{1}$ is a value.
By the inversion lemma (9), we know that there exists a term $t^{\prime}_{1}$
and $t_{1}=\lambda p.t^{\prime}_{1}$. Thus, we can apply two rules to $t$ as
follows.

      * *

Case (E-abs1)

(E-abs1) $(\lambda x.t^{\prime}_{1})\,t_{2}\leadsto(t_{2}\rhd
x)\,t^{\prime}_{1}$ $\underbrace{(\lambda
x.t^{\prime}_{1})\,t_{2}}_{t}\longrightarrow(t_{2}\rhd x)\,t^{\prime}_{1}$

Furthermore, we know the following:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}(t_{2}\rhd
x)\,t^{\prime}_{1}=[t_{2}/x]t^{\prime}_{1}\end{array}}$
($\rhd_{\mathrm{var}}$)

By choosing $t^{\prime}=[t_{2}/x]t^{\prime}_{1}$, we obtain the conclusion of
the theorem.

      * *

Case (E-abs2)

E-abs2 $(\lambda[x].t^{\prime}_{1})\,t_{2}\leadsto\textbf{let
}[x]=t_{2}\textbf{ in }t_{1}^{\prime}$
$\underbrace{(\lambda[x].t^{\prime}_{1})\,t_{2}}_{t}\longrightarrow\underbrace{\textbf{let
}[x]=t_{2}\textbf{ in }t_{1}^{\prime}}_{t^{\prime}}$

By choosing $t^{\prime}=\textbf{let }[x]=t_{2}\textbf{ in }t_{1}^{\prime}$, we
obtain the conclusion of the theorem.

    * –

Suppose $t_{1}$ is not a value.
There exists a term $t^{\prime}_{1}$ such that:

Also, we can apply evaluation for application to $t$.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}t_{1}\leadsto
t^{\prime}_{1}\end{array}}{\begin{array}[]{@{}c@{}}\underbrace{t_{1}\,t_{2}}_{t}\longrightarrow
t^{\prime}_{1}\,t_{2}\end{array}}$

Thus, by choosing $t^{\prime}=t^{\prime}_{1}\,t_{2}$, we obtain the conclusion
of the theorem.

  * •

Case (let)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\emptyset\,\vdash\,t_{1}:\Box_{r}A\quad
x:[A]_{r}\,\vdash\,t_{2}:B\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\,\vdash\,\textbf{let
}[x]=t_{1}\textbf{ in }t_{2}:B\end{array}}$ (let)

There are two cases whether $t_{1}$ is a value or not.

    * –

Suppose $t_{1}$ is a value.
By the inversion lemma (9), we know that $t_{1}$ has either a form of
$[t^{\prime}_{1}]$ or and $\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}$.

      * *

Case $t_{1}=[t_{1}^{\prime}]$.
In this case, we can apply (E-clet) to obtain the following.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\\\
\end{array}}{\begin{array}[]{@{}c@{}}\textbf{let }[x]=[t_{1}^{\prime}]\textbf{
in }t_{2}\leadsto([t_{1}^{\prime}]\rhd[x])t_{2}\end{array}}$ (E-clet)

Thus, we can apply ($\rhd_{\square}$) and ($\rhd_{\textnormal{var}}$) to
obtain the following.

($\rhd_{\textnormal{var}}$) $(t_{1}^{\prime}\rhd
x)t_{2}=[t_{1}^{\prime}/x]t_{2}$ ($\rhd_{\square}$)
$([t_{1}^{\prime}]\rhd[x])t_{2}=[t_{1}^{\prime}/x]t_{2}$

Thus, by choosing $t^{\prime}=[t^{\prime}_{1}/x]t_{2}$, we obtain the
conclusion of the theorem.

      * *

Case $t_{1}=\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}$.
In this case, we can apply (E-clet) to obtain the following:

(E-clet) $\textbf{let }[x]=\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}\textbf{
in
}t_{2}\leadsto(\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle\rhd[x])t_{2}$
$\underbrace{\textbf{let
}[x]=\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}\textbf{ in
}t_{2}}_{t}\longrightarrow(\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle\rhd[x])t_{2}$

Also, we can apply ($\rhd_{\textnormal{ver}}$) and ($\rhd_{\textnormal{var}}$)
to obtain the following.

($\rhd_{\textnormal{var}}$)
$(\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle\rhd
x)t_{2}=[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}$
($\rhd_{\textnormal{ver}}$)
$(\\{\overline{l_{i}=t^{\prime\prime}_{i}}\\}\rhd[x])t_{2}=[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}$

Thus, by choosing
$t^{\prime}=[\langle\overline{l_{i}=t^{\prime\prime}_{i}}\,|\,l_{k}\rangle/x]t_{2}$,
we obtain the conclusion of the theorem.

    * –

Suppose $t_{1}$ is not a value.
There exists terms $t^{\prime}_{1}$ such that:

Also, we can apply evaluation for contextual let bindings to $t$.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}t_{1}\leadsto
t^{\prime}_{1}\end{array}}{\begin{array}[]{@{}c@{}}\underbrace{\textbf{let
}[x]=t_{1}\textbf{ in }t_{2}}_{t}\longrightarrow\textbf{let
}[x]=t^{\prime}_{1}\textbf{ in }t_{2}\end{array}}$

Thus, by choosing $t^{\prime}=(\textbf{let }[x]=t^{\prime}_{1}\textbf{ in
}t_{2})$, we obtain the conclusion of the theorem.

  * •

Case (weak)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\emptyset\vdash
t:A\quad\vdash\emptyset\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash
t:A\end{array}}$ (weak)

In this case, $t$ does not change between before and after the last
derivation. Thus, we can obtain the conclusion of the theorem by induction
hypothesis.

  * •

Case (der)
This case hold trivially because $\Gamma_{1},x:[B]_{1}$ cannot be $\emptyset$.

  * •

Case (pr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\emptyset\vdash t:B\quad\vdash
r\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash[t]:\Box_{r}B\end{array}}$
(pr)

This case holds trivially because $[t]$ is a value.

  * •

Case (ver)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\emptyset\vdash
t_{i}:A\quad\vdash\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash\\{\overline{l_{i}=t_{i}}\\}:\Box_{\\{\overline{l_{i}}\\}}A\end{array}}$
(ver)

This case holds trivially because $\\{\overline{l_{i}=t_{i}}\\}$ is a value.

  * •

Case (veri)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\emptyset\vdash
t_{i}:A\quad\vdash\\{\overline{l_{i}}\\}\quad
l_{k}\in\\{\overline{l_{i}}\\}\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle:A\end{array}}$
(veri)

In this case, we can apply (E-veri).

(E-veri) $\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle\leadsto t_{k}@l_{k}$
$\langle\overline{l_{i}=t_{i}}\,|\,l_{k}\rangle\longrightarrow t_{k}@l_{k}$

Thus, by choosing $t^{\prime}=t_{k}@l_{k}$, we obtain the conclusion of the
theorem.

  * •

Case (extr)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\emptyset\vdash
t_{1}:\Box_{r}A\quad l_{k}\in
r\end{array}}{\begin{array}[]{@{}c@{}}\emptyset\vdash
t_{1}.l_{k}:A\end{array}}$ (extr)

In this case, we have two cases whether $t_{1}$ is a value or not.

    * –

Suppose $t_{1}$ is a value. ($t_{1}=v_{1}$)
By Lemma 11, we know the following:

$\displaystyle\emptyset\,\vdash\,v_{1}:\Box_{r}A\hskip
10.00002pt\Longrightarrow\hskip 10.00002pt\exists
t^{\prime}.\left\\{\begin{aligned} &v_{1}.l_{k}\longrightarrow t^{\prime}\\\
&\emptyset\vdash t^{\prime}:A\end{aligned}\right.$

Thus, we obtain the conclusion of the theorem.

    * –

Suppose $t_{1}$ is not a value.
There exists a term $t_{1}$ such that:

Also, we can apply an exaluation rule for extraction to $t$.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}t_{1}\leadsto
t^{\prime}_{1}\end{array}}{\begin{array}[]{<EMAIL_ADDRESS>t^{\prime}_{1}.l_{k}\end{array}}$

Thus, by choosing $t^{\prime}=t_{1}^{\prime}.l_{k}$, we obtain the conclusion
of the theorem.

  * •

Case (sub)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{r},\Gamma_{2}\vdash
t:A\quad r\sqsubseteq s\quad\vdash
s\end{array}}{\begin{array}[]{@{}c@{}}\Gamma_{1},x:[B]_{s},\Gamma_{2}\vdash
t:A\end{array}}$ (sub)

In this case, $t$ does not change between before and after the last
derivation. Thus, by induction hypothesis, we obtain the conclusion of the
theorem.

##  Appendix 0.D VLMini Proofs

######  Definition 7 (Solution of Algorithmic Type Synthesis)

Suppose that $\Sigma;\Gamma\vdash t\Rightarrow
A;\Sigma^{\prime};\Delta;\Theta;\mathcal{C}$. A solution for this judgement is
a pair $(\theta,\eta,B)$ such that $\theta$ satisfies $\Theta$, $\eta$
satisfies $\mathcal{C}$, and $\theta\eta A$ = $B$.

######  Definition 8 (Solution of Pattern Type Synthesis)

Suppose that $\Sigma;R\vdash
p:A\rhd\Gamma;\Sigma^{\prime};\Theta;\mathcal{C}$. A solution for this
judgement is a pair $(\eta,\theta,B)$ such that $\theta$ satisfies $\Theta$,
$\eta$ satisfies $\mathcal{C}$, and $\theta\eta A$ = $B$.

######  Lemma 12 (Relation of Resource Well-formedness)

$\displaystyle\vdash\Sigma\;\land\;\Sigma\vdash\eta\;\land\;FTV(r)\subseteq\mathrm{dom}(\eta)\;\land\;\Sigma\vdash
r:\textnormal{{Labels}}\quad\Longrightarrow\quad\vdash\eta r$

###### Proof

Straightforward by induction on the derivation of $\Sigma\vdash
r:\textnormal{{Labels}}$.

######  Lemma 13 (Relation of Type Well-formedness)

$\displaystyle\begin{aligned}
\vdash\Sigma\;\land\;\Sigma\vdash\theta\;\land\;\Sigma\vdash\eta\;\land\;\\\
FTV(A)\subseteq\mathrm{dom}(\theta)\cup\mathrm{dom}(\eta)\;\land\;\Sigma\vdash
A:\textnormal{{Type}}\end{aligned}\quad\Longrightarrow\quad\vdash\eta\theta A$

###### Proof

Straightforward by induction on the derivation of $\Sigma\vdash
A:\textnormal{{Type}}$. The proof uses Lemma 12.

######  Lemma 14 (Relation of Type Environment Well-formedness)

$\displaystyle\begin{aligned}
\vdash\Sigma\;\land\;\Sigma\vdash\theta\;\land\;\Sigma\vdash\eta\;\land\;\\\
FTV(\Gamma)\subseteq\mathrm{dom}(\theta)\cup\mathrm{dom}(\eta)\;\land\;\Sigma\vdash\Gamma\end{aligned}\quad\Longrightarrow\quad\vdash\eta\theta\Gamma$

###### Proof

Straightforward by induction on the derivation of $\Sigma\vdash\Gamma$. The
proof uses Lemmas 12 and 13.

######  Lemma 15 (Relation of Resource Environment Well-formedness)

$\displaystyle\vdash\Sigma\;\land\;\Sigma\vdash\eta\;\land\;FTV(R)\subseteq\mathrm{dom}(\eta)\;\land\;\Sigma\vdash
R\quad\Longrightarrow\quad\vdash\eta R$

###### Proof

Straightforward by induction on the derivation of $\Sigma\vdash R$. The proof
uses Lemma 12.

######  Lemma 16 (Soundness of Pattern Type Synthesis)

$\displaystyle\left.\begin{aligned} \Sigma;R\vdash
p:A\rhd\Gamma;\Sigma^{\prime};\Theta;\mathcal{C}\\\ (\theta,\eta,\eta\theta
A)\textnormal{ is its
solution}\end{aligned}\right\\}\quad\Longrightarrow\quad\eta R\vdash
p:\eta\theta A\rhd\eta\theta\Gamma$

###### Proof

By induction on the derivation of $\Sigma;R\vdash
p:A\rhd\Gamma;\Sigma^{\prime};\Theta;\mathcal{C}$. We perform case analysis on
the rule applied last to derive $\Sigma;R\vdash
p:A\rhd\Gamma;\Sigma^{\prime};\Theta;\mathcal{C}$.

  * •

Case (pInt):

We are given

$\displaystyle
p=n,\quad\Gamma=\emptyset,\quad\Theta=\\{A\sim\textnormal{{Int}}\\},\quad\mathcal{C}=\top~{}.$

Hence, we have $\theta A=\textnormal{{Int}}$ and $\eta=\emptyset$, therefore,

$\displaystyle\eta\theta
A=\textnormal{{Int}},\quad\eta\theta\Gamma=\emptyset~{}.$

By Lemma 15,

$\displaystyle\vdash\eta R~{}.$

Therefore, by pInt,

  * •

Case (pVar), and ([pVar]):
Similarly to the case (pInt). We use lemma 13 for the case (pVar), and lemmas
12 and 13 for the case ([pVar]).

  * •

Case (p$\square$):

We are given

$\displaystyle R=-,\quad
p=[p^{\prime}],\quad\Theta=\Theta^{\prime}\land\\{A\sim\Box_{\alpha}\beta\\}~{}.$

Hence, we have $\theta$ unify $\Theta^{\prime}$, $\theta
A=\theta(\Box_{\alpha}\beta)$, and $\eta\theta
A=\eta\theta(\Box_{\alpha}\beta)$, therefore,

$\displaystyle\eta\theta A=\eta\theta(\Box_{\alpha}\beta)=\eta\theta
A,\quad\eta R=-~{}.$

Hence, by the induction hypothesis,

$\displaystyle\eta\alpha\vdash p^{\prime}:\eta\theta\beta\rhd\eta\theta\Gamma$

Therefore, by p$\square$,

Since $\theta$ does not include type substituions for resource variables,
$\eta\alpha=\eta\theta\alpha$, hence
$\Box_{\eta\alpha}\eta\theta\beta=\eta\theta(\Box_{\alpha}\beta)=\eta\theta
A$. Therefore, we get the conclusion for this case.

######  Theorem 0.D.1 (Soundness of Algorithmic Type Synthesis)

$\displaystyle\left.\begin{aligned} \Sigma;\Gamma\vdash t\Rightarrow
A;\Sigma^{\prime};\Delta;\Theta;\mathcal{C}\\\ (\theta,\eta,\eta\theta
A)\textnormal{ is its
solution}\end{aligned}\right\\}\quad\Longrightarrow\quad\eta\theta\Delta\vdash
t:\eta\theta A$

###### Proof

By induction on the derivation of $\Sigma;\Gamma\vdash t\Rightarrow
A;\Sigma^{\prime};\Delta;\Theta;\mathcal{C}$. We perform case analysis on the
rule applied last to derive $\Sigma;\Gamma\vdash t\Rightarrow
A;\Sigma^{\prime};\Delta;\Theta;\mathcal{C}$.

  * •

Case ($\Rightarrow_{\textsc{int}}$):

We are given

$\displaystyle t=n,\quad
A=\textnormal{{Int}},\quad\Delta=\emptyset,\quad\Theta=\top,\quad\mathcal{C}=\top~{}.$

Hence, we have $\theta=\emptyset$ and $\eta=\emptyset$, therefore,

$\displaystyle\eta\theta\Delta=\emptyset,\quad\eta\theta
A=\textnormal{{Int}}~{}.$

Therefore, by (int),

  * •

Case ($\Rightarrow_{\textsc{lin}}$):

We are given

$\displaystyle t=x,\quad\Delta=x:A,\quad\Theta=\top,\quad\mathcal{C}=\top~{}.$

Hence, we have $\theta=\emptyset$ and $\eta=\emptyset$, therefore,

$\displaystyle\eta\theta\Delta=x:A,\quad\eta\theta A=A~{}.$

Furthermore, by Lemma 13, we have

$\displaystyle\vdash\eta\theta A~{}(=A)~{}.$

Therefore, by (var),

  * •

Case ($\Rightarrow_{\textsc{gr}}$):

We are given

$\displaystyle
t=x,\quad\Delta=x:[A]_{1},\quad\Theta=\top,\quad\mathcal{C}=\top~{}.$

Hence, we have $\theta=\emptyset$ and $\eta=\emptyset$, therefore,

$\displaystyle\eta\theta\Delta=x:[A]_{1},\quad\eta\theta A=A~{}.$

Furthermore, by Lemma 13, we have

$\displaystyle\vdash\eta\theta A~{}(=A)~{}.$

Therefore, we conclude the case by the following derivation.

(var) $x:A\vdash x:A$ (der) $x:[A]_{1}\vdash x:A$

  * •

Case ($\Rightarrow_{\textsc{abs}}$):

We are given

$\displaystyle t=\alpha\rightarrow
B,\quad\Delta=\Delta^{\prime}\backslash\Gamma^{\prime},\quad\Theta=\Theta_{1}\land\Theta_{2},~{}.$

Hence, we have $\theta$ unifies $\Theta_{1}$ and $\Theta_{2}$, $\eta$ unifies
$\mathcal{C}$. Therefore, we have

$\displaystyle\eta\theta\Delta=\eta\theta(\Delta^{\prime}\backslash\Gamma^{\prime}),\quad\eta\theta
A=\eta\theta(\alpha\rightarrow B)~{}.$

Furthermore, by Lemma 16 and the induction hypothesis, we have

$\displaystyle-\vdash
p:\eta\theta\alpha\rhd\eta\theta\Gamma^{\prime},\quad\eta\theta\Delta^{\prime}\vdash
t:\eta\theta B~{}.$

Therefore, by (abs),

Since
$\eta\theta\Delta^{\prime}\backslash\eta\theta\Gamma^{\prime}=\eta\theta(\Delta^{\prime}\backslash\Gamma^{\prime})$
and $\eta\theta\alpha\rightarrow\eta\theta B=\eta\theta(\alpha\rightarrow B)$,
we have the conclusion of the case.

  * •

Case ($\Rightarrow_{\textsc{app}}$):

We are given

$\displaystyle t=t_{1}\,t_{2},\quad
A=\beta,\quad\Delta=\Delta_{2}+\Delta_{2},$
$\displaystyle\Theta=\Theta_{1}\land\Theta_{2}\land\\{A_{1}\sim
A_{2}\rightarrow\beta\\},\quad\mathcal{C}=\mathcal{C}_{1}\land\mathcal{C}_{2}~{}.$

Hence, we have $\theta$ unifies $\Theta_{1}$ and $\Theta_{2}$, and $\theta
A_{1}=\theta(A_{2}\rightarrow\beta)$. Also, $\eta$ unifies $\mathcal{C}_{1}$
and $\mathcal{C}_{2}$, and then we have $\eta\theta
A_{1}=\eta\theta(A_{2}\rightarrow\beta)=\eta\theta
A_{2}\rightarrow\eta\theta\beta$. Therefore, we have

$\displaystyle\eta\theta\Delta=\eta\theta(\Delta_{2}+\Delta_{2}),\quad\eta\theta
A=\eta\theta\beta~{}.$

Furthermore, by the induction hypothesises,

$\displaystyle\eta\theta\Gamma\vdash t_{1}:\eta\theta A_{1}~{}(=\eta\theta
A_{2}\rightarrow\eta\theta\beta),\quad\eta\theta\Gamma\vdash t_{2}:\eta\theta
A_{2}~{}.$

Therefore, by (app),

  * •

Case ($\Rightarrow_{\textsc{pr}}$):

We are given

$\displaystyle t=[t],\quad
A=\Box_{\alpha}A^{\prime},\quad\Delta=\alpha\cdot\Delta^{\prime},\quad\mathcal{C}=\mathcal{C}_{1}\land\mathcal{C}_{2},~{}.$

Hence, $\theta$ unifies $\Theta$ and $\eta$ unifies $\mathcal{C}_{1}$ and
$\mathcal{C}_{2}$. Therefore, we have

$\displaystyle\eta\theta\Delta=\eta\theta(\alpha\cdot\Delta^{\prime})=(\eta\theta\alpha)\cdot(\eta\theta\Delta^{\prime}),\quad\eta\theta
A=\eta\theta(\Box_{\alpha}A^{\prime})=\Box_{\eta\theta\alpha}\eta\theta
A^{\prime}~{}.$

Furthermore, by the induction hypothesis, we have

$\displaystyle\eta\theta\Delta^{\prime}\vdash t:\eta\theta A^{\prime}~{}.$

Therefore, by (pr),