$\begin{array}[]{rcl}(x==_{\texttt{()}}\texttt{unit})[e/x]&=&\texttt{unit}==_{\texttt{()}}\texttt{unit}\\\
&\hookrightarrow&(==_{(\texttt{unit},\texttt{()})})\ \texttt{unit}\\\
&\hookrightarrow&\texttt{unit}=\texttt{unit}\\\ &=&\texttt{true}\end{array}$

  * •

$==_{b}\in\left[\\!\left|{x}\text{:}{b}\rightarrow{y}\text{:}{b}\rightarrow\\{{z}\text{:}{\texttt{Bool}}\mid{z==_{\texttt{Bool}}(x==_{b}y)}\\}\right|\\!\right]$.
By the definition of interpretation of function types, we fix
$e_{x},e_{y}\in\left[\\!\left|b\right|\\!\right]$ and we need to prove that
$e\equiv
e_{x}==_{b}e_{y}\in\left[\\!\left|(\\{{z}\text{:}{\texttt{Bool}}\mid{z==_{\texttt{Bool}}(x==_{b}y)}\\})[e_{x}/x][e_{y}/y]\right|\\!\right]$.
We prove the below three requirements of membership in the interpretation of
basic types:

    * –

$e\hookrightarrow^{*}v$, which holds because

$\begin{array}[]{rcll}e&=&e_{x}==_{b}e_{y}&\\\
&\hookrightarrow^{*}&v_{x}==_{b}e_{y}&\text{because
}e_{x}\in\left[\\!\left|b\right|\\!\right]\\\
&\hookrightarrow^{*}&v_{x}==_{b}v_{y}&\text{because
}e_{y}\in\left[\\!\left|b\right|\\!\right]\\\
&\hookrightarrow&(==_{(v_{x},b)})\ v_{y}&\\\ &\hookrightarrow&v_{x}=v_{y}&\\\
&=&v&\text{with }v=\texttt{true}\text{ or }v=\texttt{false}\end{array}$

    * –

$\vdash_{B}e\,\mathrel{::}\,\texttt{Bool}$, which holds by the typing rule
BTCon and because $e_{x},e_{y}\in\left[\\!\left|b\right|\\!\right]$ thus
$\vdash_{B}e_{x}\,\mathrel{::}\,b$ and $\vdash_{B}e_{y}\,\mathrel{::}\,b$; and

    * –

$(z==_{\texttt{Bool}}(x==_{b}y))[e/z][e_{x}/x][e_{y}/y]\hookrightarrow^{*}\texttt{true}$.
Since $e_{x},e_{y}\in\left[\\!\left|b\right|\\!\right]$ both expressions
evaluate to values, say $e_{x}\hookrightarrow^{*}v_{x}$ and
$e_{y}\hookrightarrow^{*}v_{y}$ which holds because

$\begin{array}[]{rcll}(z==_{\texttt{Bool}}(x==_{b}y))[e/z][e_{x}/x][e_{y}/y]&=&e==_{\texttt{Bool}}(e_{x}==_{b}e_{y})&\\\
&=&(e_{x}==_{b}e_{y})==_{\texttt{Bool}}(e_{x}==_{b}e_{y})&\\\
&\hookrightarrow^{*}&(v_{x}==_{b}e_{y})==_{\texttt{Bool}}(e_{x}==_{b}e_{y})&\text{since
}e_{x}\hookrightarrow^{*}v_{x}\\\
&\hookrightarrow^{*}&(v_{x}==_{b}v_{y})==_{\texttt{Bool}}(e_{x}==_{b}e_{y})&\text{since
}e_{y}\hookrightarrow^{*}v_{y}\\\ &\hookrightarrow&((==_{(v_{x},b)})\
v_{y})==_{\texttt{Bool}}(e_{x}==_{b}e_{y})&\\\
&\hookrightarrow&(v_{x}=v_{y})==_{\texttt{Bool}}(e_{x}==_{b}e_{y})&\\\
&\hookrightarrow^{*}&(v_{x}=v_{y})==_{\texttt{Bool}}(v_{x}==_{b}e_{y})&\text{since
}e_{x}\hookrightarrow^{*}v_{x}\\\
&\hookrightarrow^{*}&(v_{x}=v_{y})==_{\texttt{Bool}}(v_{x}==_{b}v_{y})&\text{since
}e_{y}\hookrightarrow^{*}v_{y}\\\
&\hookrightarrow&(v_{x}=v_{y})==_{\texttt{Bool}}((==_{(v_{x},b)})\ v_{y})&\\\
&\hookrightarrow&(v_{x}=v_{y})==_{\texttt{Bool}}(v_{x}=v_{y})&\\\
&\hookrightarrow&(v_{x}=v_{y})==_{\texttt{Bool}}(v_{x}=v_{y})&\\\
&\hookrightarrow&((==_{((v_{x}=v_{y}),\texttt{Bool})})\ (v_{x}=v_{y})&\\\
&\hookrightarrow&(v_{x}=v_{y})=(v_{x}=v_{y})&\\\ &=&\texttt{true}&\\\
\end{array}$

∎

###  B.3. Type Soundness

###### Theorem B.2 (Semantic soundness).

If $\Gamma\vdash e\mathrel{\text{::}}\tau$ then $\Gamma\models e\in\tau$.

###### Proof.

By induction on the typing derivation.

  * TSub

By inversion of the rule we have

    1. (1)

$\Gamma\vdash e\mathrel{\text{::}}\tau^{\prime}$

    2. (2)

${\Gamma}\vdash{\tau^{\prime}}\ \preceq\ {\tau}$

By IH on (1) we have

    1. (3)

$\Gamma\models e\in\tau^{\prime}$

By Theorem B.6 and (2) we have

    1. (4)

${\Gamma}\vdash{\tau^{\prime}}\ \subseteq\ {\tau}$

By (3), (4), and the definition of subsets we directly get $\Gamma\models
e\in\tau$.

  * TSelf

Assume $\Gamma\vdash e\mathrel{\text{::}}\\{{z}\text{:}{b}\mid{z==_{b}e}\\}$.
By inversion we have

    1. (1)

$\Gamma\vdash e\mathrel{\text{::}}\\{{z}\text{:}{b}\mid{r}\\}$

By IH we have

    1. (2)

$\Gamma\models e\in\\{{z}\text{:}{b}\mid{r}\\}$

We fix $\theta\in\left[\\!\left|\Gamma\right|\\!\right]$. By the definition of
semantic typing we get

    1. (3)

${\theta}\cdot{e}\in\left[\\!\left|{\theta}\cdot{\\{{z}\text{:}{b}\mid{r}\\}}\right|\\!\right]$

By the definition of denotations on basic types we have

    1. (4)

${\theta}\cdot{e}\hookrightarrow^{*}v$

    2. (5)

$\vdash_{B}{\theta}\cdot{e}\,\mathrel{::}\,b$

    3. (6)

${\theta}\cdot{r}[{\theta}\cdot{e}/z]\hookrightarrow^{*}\texttt{true}$

Since $\theta$ contains values, by the definition of $==_{b}$ we have

    1. (7)

${\theta}\cdot{e}==_{b}{\theta}\cdot{e}\hookrightarrow^{*}\texttt{true}$

Thus

    1. (8)

${\theta}\cdot{(z==_{b}e)}[{\theta}\cdot{e}/z]\hookrightarrow^{*}\texttt{true}$

By (4), (5), and (8) we have

    1. (9)

${\theta}\cdot{e}\in\left[\\!\left|{\theta}\cdot{\\{{z}\text{:}{b}\mid{z==_{b}e}\\}}\right|\\!\right]$

Thus, $\Gamma\models e\in\\{{z}\text{:}{b}\mid{z==_{b}e}\\}$.

  * TCon

This case holds exactly because of Property B.1.

  * TVar

This case holds by the definition of closing substitutions.

  * TLam

Assume $\Gamma\vdash\lambda
x\mathord{:}\tau_{x}.~{}e\mathrel{\text{::}}{x}\text{:}{\tau_{x}}\rightarrow\tau$.
By inversion of the rule we have $\Gamma,x:\tau_{x}\vdash
e\mathrel{\text{::}}\tau$. By IH we get $\Gamma,x:\tau_{x}\models e\in\tau$.

We need to show that $\Gamma\models\lambda
x\mathord{:}\tau_{x}.~{}e\in{x}\text{:}{\tau_{x}}\rightarrow\tau$. Which, for
some $\theta\in\left[\\!\left|\Gamma\right|\\!\right]$ is equivalent to
$\lambda x\mathord{:}{\theta}\cdot{\tau_{x}}.~{}{\theta}\cdot{e}$ $\in$
$\left[\\!\left|{x}\text{:}{{\theta}\cdot{\tau_{x}}}\rightarrow{\theta}\cdot{\tau}\right|\\!\right]$.

We pick a random
$e_{x}\in\left[\\!\left|{\theta}\cdot{\tau_{x}}\right|\\!\right]$ thus we need
to show that ${\theta}\cdot{e[e_{x}/x]}$ $\in$
$\left[\\!\left|{\theta}\cdot{\tau[e_{x}/x]}\right|\\!\right]$. By Lemma B.3,
there exists $v_{x}$ so that $e_{x}\hookrightarrow^{*}v_{x}$ and
$v_{x}\in\left[\\!\left|\tau_{x}\right|\\!\right]$. By the inductive
hypothesis, ${\theta}\cdot{e[v_{x}/x]}$ $\in$
$\left[\\!\left|{\theta}\cdot{\tau[v_{x}/x]}\right|\\!\right]$. By Lemma B.4,
${\theta}\cdot{e[e_{x}/x]}$ $\in$
$\left[\\!\left|{\theta}\cdot{\tau[e_{x}/x]}\right|\\!\right]$, which
concludes our proof.

  * TApp

Assume $\Gamma\vdash e\ e_{x}\mathrel{\text{::}}\tau[e_{x}/x]$. By inversion
we have

    1. (1)

$\Gamma\vdash e\mathrel{\text{::}}{x}\text{:}{\tau_{x}}\rightarrow\tau$

    2. (2)

$\Gamma\vdash e_{x}\mathrel{\text{::}}\tau_{x}$

By IH we get

    1. (3)

$\Gamma\models e\in{x}\text{:}{\tau_{x}}\rightarrow\tau$

    2. (4)

$\Gamma\models e_{x}\in\tau_{x}$

We fix $\theta\in\left[\\!\left|\Gamma\right|\\!\right]$. By the definition of
semantic types

    1. (5)

${\theta}\cdot{e}$ $\in$
$\left[\\!\left|{\theta}\cdot{{x}\text{:}{\tau_{x}}\rightarrow\tau}\right|\\!\right]$

    2. (6)

${\theta}\cdot{e_{x}}$ $\in$
$\left[\\!\left|{\theta}\cdot{\tau_{x}}\right|\\!\right]$

By (5), (6), and the definition of semantic typing on functions:

    1. (7)

${\theta}\cdot{e\ e_{x}}$ $\in$
$\left[\\!\left|{\theta}\cdot{\tau[e_{x}/x]}\right|\\!\right]$

Which directly leads to the required $\Gamma\models e\ e_{x}\in\tau[e_{x}/x]$

  * TEqBase

Assume $\Gamma\vdash\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e\mathrel{\text{::}}\texttt{PEq}_{b}\ \\{e_{l}\\}\ \\{e_{r}\\}$. By inversion
we get:

    1. (1)

$\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{l}$

    2. (2)

$\Gamma\vdash e_{r}\mathrel{\text{::}}\tau_{r}$

    3. (3)

${\Gamma}\vdash{\tau_{l}}\ \preceq\ {\\{{x}\text{:}{b}\mid{\texttt{true}}\\}}$

    4. (4)

${\Gamma}\vdash{\tau_{r}}\ \preceq\ {\\{{x}\text{:}{b}\mid{\texttt{true}}\\}}$

    5. (5)

$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
e\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$

By IH we get

    1. (4)

$\Gamma\models e_{l}\in\tau_{l}$

    2. (5)

$\Gamma\models e_{r}\in\tau_{r}$

    3. (6)

$\Gamma,r:\tau_{r},l:\tau_{l}\models
e\in\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$

We fix $\theta\in\left[\\!\left|\Gamma\right|\\!\right]$. Then (4) and (5)
become

    1. (7)

${\theta}\cdot{e_{l}}$ $\in$
$\left[\\!\left|{\theta}\cdot{\tau_{l}}\right|\\!\right]$

    2. (8)

${\theta}\cdot{e_{r}}$ $\in$
$\left[\\!\left|{\theta}\cdot{\tau_{r}}\right|\\!\right]$

    3. (9)

$\Gamma\models e_{r}\in\tau_{r}$

    4. (10)

$\Gamma,r:\tau_{r},l:\tau_{l}\models
e\in\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$

Assume

    1. (11)

${\theta}\cdot{e_{l}}\hookrightarrow^{*}v_{l}$

    2. (12)

${\theta}\cdot{e_{r}}\hookrightarrow^{*}v_{r}$

By (7), (8), (11), (12), and Lemma B.3 we get

    1. (13)

$v_{l}\in\left[\\!\left|{\theta}\cdot{\tau_{l}}\right|\\!\right]$

    2. (14)

$v_{r}\in\left[\\!\left|{\theta}\cdot{\tau_{r}}\right|\\!\right]$

By (10), (11), and (12) we get

    1. (15)

$v_{l}==_{b}v_{r}\hookrightarrow^{*}\texttt{true}$

By (11), (12), (15), ane Lemma B.5 we have

    1. (16)

${\theta}\cdot{e_{l}}==_{b}{\theta}\cdot{e_{r}}\hookrightarrow^{*}\texttt{true}$

By (1-5) we get:

    1. (17)

$\vdash_{B}{\theta}\cdot{\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e}\,\mathrel{::}\,\texttt{PBEq}_{b}$

Trivially, with zero evaluation steps we have:

    1. (18)

${\theta}\cdot{\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e}\hookrightarrow^{*}\texttt{bEq}_{b}\ ({{\theta}\cdot{e_{l}}})\
({{\theta}\cdot{e_{l}}})\ ({{\theta}\cdot{e}})$

By (16), (17), (18) and the definition of semantic types on basic equality
types we have

    1. (19)

${\theta}\cdot{\texttt{bEq}_{b}\ e_{l}\ e_{r}\ e}$ $\in$
$\left[\\!\left|{\theta}\cdot{\texttt{PEq}_{b}\ \\{e_{l}\\}\
\\{e_{r}\\}}\right|\\!\right]$

Which leads to the required $\Gamma\models\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e\in\texttt{PEq}_{b}\ \\{e_{l}\\}\ \\{e_{r}\\}$.

  * TEqFun

Assume $\Gamma\vdash\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
e_{l}\ e_{r}\
e\mathrel{\text{::}}\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}$. By inversion we have

    1. (1)

$\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{l}$

    2. (2)

$\Gamma\vdash e_{r}\mathrel{\text{::}}\tau_{r}$

    3. (3)

${\Gamma}\vdash{\tau_{l}}\ \preceq\ {{x}\text{:}{\tau_{x}}\rightarrow\tau}$

    4. (4)

${\Gamma}\vdash{\tau_{r}}\ \preceq\ {{x}\text{:}{\tau_{x}}\rightarrow\tau}$

    5. (5)

$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
e\mathrel{\text{::}}({x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\
\\{l\ x\\}\ \\{r\ x\\})$

    6. (6)

$\Gamma\vdash{x}\text{:}{\tau_{x}}\rightarrow\tau$

By IH and Theorem B.6 we get

    1. (7)

$\Gamma\models e_{l}\in\tau_{l}$

    2. (8)

$\Gamma\models e_{r}\in\tau_{r}$

    3. (9)

${\Gamma}\vdash{\tau_{l}}\ \subseteq\ {{x}\text{:}{\tau_{x}}\rightarrow\tau}$

    4. (10)

${\Gamma}\vdash{\tau_{r}}\ \subseteq\ {{x}\text{:}{\tau_{x}}\rightarrow\tau}$

    5. (11)

$\Gamma,r:\tau_{r},l:\tau_{l}\models
e\in({x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\ \\{l\ x\\}\ \\{r\
x\\})$

By (1-5) we get

    1. (12)

$\vdash_{B}{\theta}\cdot{\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
e_{l}\ e_{r}\
e}\,\mathrel{::}\,\texttt{PBEq}_{\lfloor{\theta}\cdot{({x}\text{:}{\tau_{x}}\rightarrow\tau)}\rfloor}$

Trivially, by zero evaluation steps, we get

    1. (13)

${\theta}\cdot{\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\
e_{r}\
e}\hookrightarrow^{*}\texttt{xEq}_{{x}\text{:}{{\theta}\cdot{\tau_{x}}}\rightarrow{\theta}\cdot{\tau}}\
({{\theta}\cdot{e_{l}}})\ ({\theta}\cdot{e_{r}})\ ({\theta}\cdot{e})$

By (7-10) we get

    1. (14)

${\theta}\cdot{e_{l}},{\theta}\cdot{e_{r}}\in\left[\\!\left|{\theta}\cdot{{x}\text{:}{\tau_{x}}\rightarrow\tau}\right|\\!\right]$

By (7), (8), (11), the definition of semantic types on functions, and Lemmata
B.3 and B.4 (similar to the previous case) we have

    * –

$\forall e_{x}\in\left[\\!\left|\tau_{x}\right|\\!\right].e\
e_{x}\in\left[\\!\left|\texttt{PEq}_{\tau[e_{x}/x]}\ \\{e_{l}\ e_{x}\\}\
\\{e_{r}\ e_{x}\\}\right|\\!\right]$

By (12), (13), (14), and (15) we get

    1. (19)

${\theta}\cdot{\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\
e_{r}\ e}$ $\in$
$\left[\\!\left|{\theta}\cdot{\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}}\right|\\!\right]$

Which leads to the required
$\Gamma\models\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\
e_{r}\ e\in\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ \\{e_{l}\\}\
\\{e_{r}\\}$.

∎

###### Lemma B.3.

If $e\in\left[\\!\left|\tau\right|\\!\right]$, then $e\hookrightarrow^{*}v$
and $v\in\left[\\!\left|\tau\right|\\!\right]$.

###### Proof.

By structural induction of the type $\tau$. ∎

###### Lemma B.4.

If $e_{x}\hookrightarrow^{*}v_{x}$ and
$e[v_{x}/x]\in\left[\\!\left|\tau[v_{x}/x]\right|\\!\right]$, then
$e[e_{x}/x]\in\left[\\!\left|\tau[e_{x}/x]\right|\\!\right]$.

###### Proof.

We can use parallel reductions (of §C) to prove that if
$e_{1}\rightrightarrows e_{2}$, then (1)
$\left[\\!\left|\tau[e_{1}/x]\right|\\!\right]=\left[\\!\left|\tau[e_{2}/x]\right|\\!\right]$
and (2) $e_{1}\in\left[\\!\left|\tau\right|\\!\right]$ iff
$e_{2}\in\left[\\!\left|\tau\right|\\!\right]$. The proof directly follows by
these two properties. ∎

###### Lemma B.5.

If $e_{x}\hookrightarrow^{*}e_{x}^{\prime}$ and
$e[e_{x}^{\prime}/x]\hookrightarrow^{*}c$, then
$e[e_{x}/x]\hookrightarrow^{*}c$.

###### Proof.

As an instance of Corollary C.17. ∎

We define semantic subtyping as follows: ${\Gamma}\vdash{\tau}\ \subseteq\
{\tau^{\prime}}$ iff
$\forall\theta\in\left[\\!\left|\Gamma\right|\\!\right].\left[\\!\left|{\theta}\cdot{\tau}\right|\\!\right]\subseteq\left[\\!\left|{\theta}\cdot{\tau^{\prime}}\right|\\!\right]$.

###### Theorem B.6 (Subtyping semantic soundness).

If ${\Gamma}\vdash{\tau}\ \preceq\ {\tau^{\prime}}$ then
${\Gamma}\vdash{\tau}\ \subseteq\ {\tau^{\prime}}$.

###### Proof.

By induction on the derivation tree:

  * SBase

Assume ${\Gamma}\vdash{\\{{x}\text{:}{b}\mid{r}\\}}\ \preceq\
{\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\}}$. By inversion
$\forall\theta\in\left[\\!\left|\Gamma\right|\\!\right],~{}\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{b}\mid{r}\\}}\right|\\!\right]\subseteq\left[\\!\left|{\theta}\cdot{\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\}}\right|\\!\right]$,
which exactly leads to the required.

  * SFun

Assume ${\Gamma}\vdash{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ \preceq\
{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}$. By inversion

    1. (1)

${\Gamma}\vdash{\tau^{\prime}_{x}}\ \preceq\ {\tau_{x}}$

    2. (2)

${\Gamma,x:\tau^{\prime}_{x}}\vdash{\tau}\ \preceq\ {\tau^{\prime}}$

By IH

    1. (3)

${\Gamma}\vdash{\tau^{\prime}_{x}}\ \subseteq\ {\tau_{x}}$

    2. (4)

${\Gamma,x:\tau^{\prime}_{x}}\vdash{\tau}\ \subseteq\ {\tau^{\prime}}$

We fix $\theta\in\Gamma$. We pick $e$. We assume
$e\in\left[\\!\left|{\theta}\cdot{{x}\text{:}{\tau_{x}}\rightarrow\tau}\right|\\!\right]$
and we will show that
$e\in\left[\\!\left|{\theta}\cdot{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}\right|\\!\right]$.
By assumption

    1. (5)

$\forall e_{x}\in\left[\\!\left|{\theta}\cdot{\tau_{x}}\right|\\!\right]\\!.\
e\ e_{x}\in\left[\\!\left|{\theta}\cdot{\tau[e_{x}/x]}\right|\\!\right]$

We need to show $\forall
e_{x}\in\left[\\!\left|{\theta}\cdot{\tau^{\prime}_{x}}\right|\\!\right]\\!.\
e\
e_{x}\in\left[\\!\left|{\theta}\cdot{\tau^{\prime}[e_{x}/x]}\right|\\!\right]$.
We fix $e_{x}$. By (3), if
$e_{x}\in\left[\\!\left|{\theta}\cdot{\tau^{\prime}_{x}}\right|\\!\right]$,
then $e_{x}\in\left[\\!\left|{\theta}\cdot{\tau_{x}}\right|\\!\right]$ and (5)
applies, so $e\
e_{x}\in\left[\\!\left|{\theta}\cdot{\tau[e_{x}/x]}\right|\\!\right]$, which
by (4) gives $e\
e_{x}\in\left[\\!\left|{\theta}\cdot{\tau^{\prime}[e_{x}/x]}\right|\\!\right]$.
Thus,
$e\in\left[\\!\left|{\theta}\cdot{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}\right|\\!\right]$.
This leads to
$\left[\\!\left|{\theta}\cdot{{x}\text{:}{\tau_{x}}\rightarrow\tau}\right|\\!\right]\subseteq\left[\\!\left|{\theta}\cdot{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}\right|\\!\right]$,
which by definition gives semantic subtyping:
${\Gamma}\vdash{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ \subseteq\
{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}$.

  * SEq

Assume ${\Gamma}\vdash{\texttt{PEq}_{\tau_{i}}\ \\{e_{l}\\}\ \\{e_{r}\\}}\
\preceq\ {\texttt{PEq}_{\tau_{i}^{\prime}}\ \\{e_{l}\\}\ \\{e_{r}\\}}$. We
split cases on the structure of $\tau_{i}$.

    * –

If  $\tau_{i}$ is a basic type, then $\tau_{i}$ is trivially refined to true.
Thus, $\tau_{i}=\tau_{i}^{\prime}=b$ and for each $\theta\in\Gamma$,
$\left[\\!\left|{\theta}\cdot{\texttt{PEq}_{\tau}\ \\{e_{l}\\}\
\\{e_{r}\\}}\right|\\!\right]=\left[\\!\left|{\theta}\cdot{\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\}}\right|\\!\right]$, thus set inclusion reduces to
equal sets.

    * –

If  $\tau_{i}$ is a function type, thus
${\Gamma}\vdash{\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}}\ \preceq\
{\texttt{PEq}_{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\}}$

By inversion

    1. (1)

${\Gamma}\vdash{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ \preceq\
{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}$

    2. (2)

${\Gamma}\vdash{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}\
\preceq\ {{x}\text{:}{\tau_{x}}\rightarrow\tau}$

By inversion on (1) and (2) we get

    1. (3)

${\Gamma}\vdash{\tau^{\prime}_{x}}\ \preceq\ {\tau_{x}}$

    2. (4)

${\Gamma,x:\tau^{\prime}_{x}}\vdash{\tau}\ \preceq\ {\tau^{\prime}}$

    3. (5)

${\Gamma,x:\tau_{x}}\vdash{\tau^{\prime}}\ \preceq\ {\tau}$

By IH on (1) and (3) we get

    1. (6)

${\Gamma}\vdash{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ \subseteq\
{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}$

    2. (7)

${\Gamma}\vdash{\tau^{\prime}_{x}}\ \subseteq\ {\tau_{x}}$

We fix $\theta\in\Gamma$ and some $e$. If
$e\in\left[\\!\left|{\theta}\cdot{\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}}\right|\\!\right]$ we need to show that
$e\in\left[\\!\left|{\theta}\cdot{\texttt{PEq}_{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\}}\right|\\!\right]$. By the assumption we have

    1. (8)

$\vdash_{B}e\,\mathrel{::}\,\texttt{PBEq}_{\lfloor{\theta}\cdot{({x}\text{:}{\tau_{x}}\rightarrow\tau)}\rfloor}$

    2. (9)

$e\hookrightarrow^{*}\texttt{xEq}_{\\_}\ ({\theta}\cdot{e_{l}})\
({\theta}\cdot{e_{r}})\ {e_{pf}}$

    3. (10)

$({\theta}\cdot{e_{l}}),({\theta}\cdot{e_{r}})\in\left[\\!\left|{\theta}\cdot{(}{x}\text{:}{\tau_{x}}\rightarrow\tau)\right|\\!\right]$

    4. (11)

$\forall
e_{x}\in\left[\\!\left|{\theta}\cdot{\tau_{x}}\right|\\!\right].e_{pf}\
e_{x}\in\left[\\!\left|\texttt{PEq}_{{\theta}\cdot{(}\tau[e_{x}/x])}\
\\{({\theta}\cdot{e_{l}})\ e_{x}\\}\ \\{({\theta}\cdot{e_{r}})\
e_{x}\\}\right|\\!\right]$

Since (8) only depends on the structure of the type index, we get

    1. (12)

$\vdash_{B}e\,\mathrel{::}\,\texttt{PBEq}_{\lfloor{\theta}\cdot{({x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime})}\rfloor}$

By (6) and (10) we get

    1. (13)

$({\theta}\cdot{e_{l}}),({\theta}\cdot{e_{r}})\in\left[\\!\left|{\theta}\cdot{(}{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime})\right|\\!\right]$

By (4), (5), Lemma B.7, the rule SEq and the IH, we get that
$\left[\\!\left|\texttt{PEq}_{{\theta}\cdot{(}\tau[e_{x}/x])}\
\\{({\theta}\cdot{e_{l}})\ e_{x}\\}\ \\{({\theta}\cdot{e_{r}})\
e_{x}\\}\right|\\!\right]\subseteq\left[\\!\left|\texttt{PEq}_{{\theta}\cdot{(}\tau^{\prime}[e_{x}/x])}\
\\{({\theta}\cdot{e_{l}})\ e_{x}\\}\ \\{({\theta}\cdot{e_{r}})\
e_{x}\\}\right|\\!\right]$. By which, (11), (7), and reasoning similar to the
SFun case, we get

    1. (14)

$\forall
e_{x}\in\left[\\!\left|{\theta}\cdot{\tau^{\prime}_{x}}\right|\\!\right].e_{pf}\
e_{x}\in\left[\\!\left|\texttt{PEq}_{{\theta}\cdot{(}\tau^{\prime}[e_{x}/x])}\
\\{({\theta}\cdot{e_{l}})\ e_{x}\\}\ \\{({\theta}\cdot{e_{r}})\
e_{x}\\}\right|\\!\right]$

By (12), (9), (13), and (14) we conclude that
$e\in\left[\\!\left|{\theta}\cdot{\texttt{PEq}_{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\}}\right|\\!\right]$, thus
${\Gamma}\vdash{\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}}\ \subseteq\
{\texttt{PEq}_{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\}}$.

∎

###### Lemma B.7 (Strengthening).

If ${\Gamma_{1}}\vdash{\tau_{1}}\ \preceq\ {\tau_{2}}$, then:

  1. (1)

If $\Gamma_{1},x:\tau_{2},\Gamma_{2}\vdash e\mathrel{\text{::}}\tau$ then
$\Gamma_{1},x:\tau_{1},\Gamma_{2}\vdash e\mathrel{\text{::}}\tau$.

  2. (2)

If ${\Gamma_{1},x:\tau_{2},\Gamma_{2}}\vdash{\tau}\ \preceq\ {\tau^{\prime}}$
then ${\Gamma_{1},x:\tau_{1},\Gamma_{2}}\vdash{\tau}\ \preceq\
{\tau^{\prime}}$.

  3. (3)

If $\Gamma_{1},x:\tau_{2},\Gamma_{2}\vdash\tau$ then
$\Gamma_{1},x:\tau_{1},\Gamma_{2}\vdash\tau$.

  4. (4)

If $\vdash\Gamma_{1},x:\tau_{2},\Gamma_{2}$ then
$\vdash\Gamma_{1},x:\tau_{1},\Gamma_{2}$.

###### Proof.

The proofs go by induction. Only the TVar case is insteresting; we use TSub
and our assumption. ∎

###### Lemma B.8 (Semantic typing is closed under parallel reduction in
expressions).

If $e_{1}\rightrightarrows^{*}e_{2}$, then
$e_{1}\in\left[\\!\left|\tau\right|\\!\right]$ iff
$e_{2}\in\left[\\!\left|\tau\right|\\!\right]$.

###### Proof.

By induction on $\tau$, using parallel reduction as a bisimulation (Lemma C.5
and Corollary C.15). ∎

###### Lemma B.9 (Semantic typing is closed under parallel reduction in
types).

If $\tau_{1}\rightrightarrows^{*}\tau_{2}$ then
$\left[\\!\left|\tau_{1}\right|\\!\right]=\left[\\!\left|\tau_{2}\right|\\!\right]$.

###### Proof.

By induction on $\tau_{1}$ (which necessarily has the same shape as
$\tau_{2}$). We use parallel reduction as a bisimulation (Lemma C.5 and
Corollary C.15). ∎

###### Lemma B.10 (Parallel reducing types are equal).

If $\Gamma\vdash\tau_{1}$ and $\Gamma\vdash\tau_{2}$ and
$\tau_{1}\rightrightarrows^{*}\tau_{2}$ then ${\Gamma}\vdash{\tau_{1}}\
\preceq\ {\tau_{2}}$ and ${\Gamma}\vdash{\tau_{1}}\ \preceq\ {\tau_{2}}$.

###### Proof.

By induction on the parallel reduction sequence; for a single step, by
induction on $\tau_{1}$ (which must have the same structure as $\tau_{2}$). We
use parallel reduction as a bisimulation (Lemma C.5 and Corollary C.15). ∎

###### Lemma B.11 (Regularity).

  1. (1)

If $\Gamma\vdash e\mathrel{\text{::}}\tau$ then $\vdash\Gamma$ and
$\Gamma\vdash\tau$.

  2. (2)

If $\Gamma\vdash\tau$ then $\vdash\Gamma$.

  3. (3)

If ${\Gamma}\vdash{\tau_{1}}\ \preceq\ {\tau_{2}}$ then $\vdash\Gamma$ and
$\Gamma\vdash\tau_{1}$ and $\Gamma\vdash\tau_{2}$.

###### Proof.

By a big ol’ induction. ∎

###### Lemma B.12 (Canonical forms).

If $\Gamma\vdash v\mathrel{\text{::}}\tau$, then:

  * •

If $\tau=\\{{x}\text{:}{b}\mid{e}\\}$, then $v=c$ such that
$\texttt{TyCon}(c)=b$ and ${\Gamma}\vdash{\texttt{TyCon}(c)}\ \preceq\
{\\{{x}\text{:}{b}\mid{e}\\}}$.

  * •

If $\tau={x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}$, then
$v=\textsc{TLam}{x}{\tau_{x}^{\prime}}{e}$ such that
${\Gamma}\vdash{\tau_{x}}\ \preceq\ {\tau_{x}^{\prime}}$ and
$\Gamma,x:\tau_{x}^{\prime}\vdash e\mathrel{\text{::}}\tau^{\prime\prime}$
such that ${\tau^{\prime\prime}}\vdash{\tau^{\prime}}\ \preceq\ {.}$

  * •

If $\tau=\texttt{PEq}_{b}\ \\{e_{l}\\}\ \\{e_{r}\\}$ then $v=\texttt{bEq}_{b}\
e_{l}\ e_{r}\ v_{p}$ such that $\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{l}$
and $\Gamma\vdash e_{r}\mathrel{\text{::}}\tau_{r}$ (for some $\tau_{l}$ and
$\tau_{r}$ that are refinements of $b$) and
$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
v_{p}\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$.

  * •

If $\tau=\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\}$ then
$v=\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime\prime}}\
e_{l}\ e_{r}\ v_{p}$ such that ${\Gamma}\vdash{\tau_{x}}\ \preceq\
{\tau_{x}^{\prime}}$ and ${\Gamma,x:\tau_{x}}\vdash{\tau^{\prime\prime}}\
\preceq\ {\tau^{\prime}}$ and $\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{l}$
and $\Gamma\vdash e_{r}\mathrel{\text{::}}\tau_{r}$ (for some $\tau_{l}$ and
$\tau_{r}$ that are subtypes of
${x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime\prime}$) and
$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
v_{p}\mathrel{\text{::}}{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\texttt{PEq}_{\tau^{\prime\prime}}\
\\{e_{l}\ x\\}\ \\{e_{r}\ x\\}$.

###  B.4. The Binary Logical Relation

###### Theorem B.13 ($\mathsf{EqRT}$ soundness).

If $\Gamma\vdash e\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{1}\\}\
\\{e_{2}\\}$, then $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$.

###### Proof.

By $\Gamma\vdash e\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{1}\\}\
\\{e_{2}\\}$ and the Fundamental Property B.22 we have $\Gamma\vdash
e\mathrel{\sim}e\,\mathrel{::}\,\texttt{PEq}_{\tau}\ \\{e_{1}\\}\
\\{e_{2}\\}$. Thus, for a fixed $\delta\in\Gamma$,
${{\delta}_{1}}\cdot{e}\mathrel{\sim}{{\delta}_{2}}\cdot{e}\mathrel{::}\texttt{PEq}_{\tau}\
\\{e_{1}\\}\ \\{e_{2}\\};{\delta}$. By the definition of the logical relation
for EqRT, we have
${{\delta}_{1}}\cdot{e_{1}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{2}}\mathrel{::}\tau;{\delta}$.
So, $\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$. ∎

###### Lemma B.14 (LR respects subtyping).

If $\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$ and
${\Gamma}\vdash{\tau}\ \preceq\ {\tau^{\prime}}$, then $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau^{\prime}$.

###### Proof.

By induction on the derivation of the subtyping tree.

  * SBase

By assumption we have

    1. (1)

$\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\\{{x}\text{:}{b}\mid{r}\\}$

    2. (2)

${\Gamma}\vdash{\\{{x}\text{:}{b}\mid{r}\\}}\ \preceq\
{\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\}}$

By inversion on (2) we get

    1. (3)

$\forall\theta\in\left[\\!\left|\Gamma\right|\\!\right],~{}\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{b}\mid{r}\\}}\right|\\!\right]\subseteq\left[\\!\left|{\theta}\cdot{\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\}}\right|\\!\right]$

We fix $\delta\in\Gamma$. By (1) we get

    1. (4)

${{\delta}_{1}}\cdot{e_{1}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{2}}\mathrel{::}\\{{x}\text{:}{b}\mid{r}\\};{\delta}$

By the definition of logical relations:

    1. (5)

${\delta_{1}}\cdot{e_{1}}\hookrightarrow^{*}v_{1}$

    2. (6)

${\delta_{2}}\cdot{e_{2}}\hookrightarrow^{*}v_{2}$

    3. (7)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\\{{x}\text{:}{b}\mid{r}\\};{\delta}$

By (7) and the definition of the logical relation on basic types we have

    1. (8)

$v_{1}=v_{2}=c$

    2. (9)

$\vdash_{B}c\,\mathrel{::}\,b$

    3. (10)

${\delta_{1}}\cdot{r[c/x]}\hookrightarrow^{*}\texttt{true}$

    4. (11)

${\delta_{2}}\cdot{r[c/x]}\hookrightarrow^{*}\texttt{true}$

By (3), (10) and (11) become

    1. (12)

${\delta_{1}}\cdot{r^{\prime}[c/x^{\prime}]}\hookrightarrow^{*}\texttt{true}$

    2. (13)

${\delta_{2}}\cdot{r^{\prime}[c/x^{\prime}]}\hookrightarrow^{*}\texttt{true}$

By (8), (9), (12), and (13) we get

    1. (14)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\};{\delta}$

By (5), (6), and (14) we have

    1. (15)

${{\delta}_{1}}\cdot{e_{1}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{2}}\mathrel{::}\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\};{\delta}$

Thus, $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\\{{x^{\prime}}\text{:}{b}\mid{r^{\prime}}\\}$.

  * SFun

By assumption:

    1. (1)

$\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,{x}\text{:}{\tau_{x}}\rightarrow\tau$

    2. (2)

${\Gamma}\vdash{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ \preceq\
{{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}}$

By inversion of the rule (2)

    1. (3)

${\Gamma}\vdash{\tau^{\prime}_{x}}\ \preceq\ {\tau_{x}}$

    2. (4)

${\Gamma,x:\tau^{\prime}_{x}}\vdash{\tau}\ \preceq\ {\tau^{\prime}}$

We fix $\delta\in\Gamma$. By (1) and the definition of logical relation

    1. (5)

${\delta_{1}}\cdot{e_{1}}\hookrightarrow^{*}v_{1}$

    2. (6)

${\delta_{2}}\cdot{e_{2}}\hookrightarrow^{*}v_{2}$

    3. (7)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

We fix $v^{\prime}_{1}$ and $v^{\prime}_{2}$ so that

    1. (8)

$v^{\prime}_{1}\mathrel{\sim}v^{\prime}_{2}\mathrel{::}\tau^{\prime}_{x};{\delta}$

By (8) and the definition of logical relations, since the values are
idempotent under substitution, we have

    1. (9)

$\Gamma\vdash
v^{\prime}_{1}\mathrel{\sim}v^{\prime}_{2}\,\mathrel{::}\,\tau^{\prime}_{x}$

By (9) and inductive hypothesis on (3) we have

    1. (10)

$\Gamma\vdash
v^{\prime}_{1}\mathrel{\sim}v^{\prime}_{2}\,\mathrel{::}\,\tau_{x}$

By (10), idempotence of values under substitution, and the definition of
logical relations, we have

    1. (11)

$v^{\prime}_{1}\mathrel{\sim}v^{\prime}_{2}\mathrel{::}\tau_{x};{\delta}$

By (7), (11), and the definition of logical relations on function values:

    1. (12)

$v_{1}\ v^{\prime}_{1}\mathrel{\sim}v_{2}\
v^{\prime}_{2}\mathrel{::}\tau;{\delta,(v^{\prime}_{1},v^{\prime}_{2})/x}$

By (9), (12), and the definition of logical relations we have

    1. (12)

$\Gamma,x:\tau^{\prime}_{x}\vdash v_{1}\ v^{\prime}_{1}\mathrel{\sim}v_{2}\
v^{\prime}_{2}\,\mathrel{::}\,\tau$

By (12) and inductive hypothesis on (4) we have

    1. (13)

$\Gamma,x:\tau^{\prime}_{x}\vdash v_{1}\ v^{\prime}_{1}\mathrel{\sim}v_{2}\
v^{\prime}_{2}\,\mathrel{::}\,\tau^{\prime}$

By (8), (13), and the definition of logical relations, we have

    1. (14)

$v_{1}\ v^{\prime}_{1}\mathrel{\sim}v_{2}\
v^{\prime}_{2}\mathrel{::}\tau^{\prime};{\delta,(v^{\prime}_{1},v^{\prime}_{2})/x}$

By (8), (14), and the definition of logical relations, we have

    1. (15)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime};{\delta}$

By (5), (6), and (15), we get

    1. (16)

${{\delta}_{1}}\cdot{e_{1}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{2}}\mathrel{::}{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime};{\delta}$

So, $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}$.

  * SEq

By hypothesis:

    1. (1)

$\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\texttt{PEq}_{\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}$

    2. (2)

${\Gamma}\vdash{\texttt{PEq}_{\tau}\ \\{e_{l}\\}\ \\{e_{r}\\}}\ \preceq\
{\texttt{PEq}_{\tau^{\prime}}\ \\{e_{l}\\}\ \\{e_{r}\\}}$

We fix $\delta\in\Gamma$. By (1)

    1. (3)

${{\delta}_{1}}\cdot{e_{1}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{2}}\mathrel{::}\texttt{PEq}_{\tau}\
\\{e_{l}\\}\ \\{e_{r}\\};{\delta}$

By (3) and the definition of logical relations.

    1. (4)

${\delta_{1}}\cdot{e_{1}}\hookrightarrow^{*}v_{1}$

    2. (5)

${\delta_{2}}\cdot{e_{2}}\hookrightarrow^{*}v_{2}$

    3. (6)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\texttt{PEq}_{\tau}\ \\{e_{l}\\}\
\\{e_{r}\\};{\delta}$

By (6) and the definition of logical relations

    1. (7)

${\delta_{1}}\cdot{e_{l}}\mathrel{\sim}{\delta_{2}}\cdot{e_{r}}\mathrel{::}\tau;{\delta}$

By (7) and the definition of logical relations.

    1. (8)

$\Gamma\vdash{e_{l}}\mathrel{\sim}{e_{r}}\,\mathrel{::}\,\tau$

By inversion on (2)

    1. (9)

${\Gamma}\vdash{\tau}\ \preceq\ {\tau^{\prime}}$

    2. (10)

${\Gamma}\vdash{\tau^{\prime}}\ \preceq\ {\tau}$

By (8) and inductive hypothesis on (9)

    1. (11)

$\Gamma\vdash{e_{l}}\mathrel{\sim}{e_{r}}\,\mathrel{::}\,\tau^{\prime}$

Thus,

    1. (12)

${{\delta}_{1}}\cdot{{e_{l}}}\mathrel{\sim}{{\delta}_{2}}\cdot{{e_{r}}}\mathrel{::}\tau^{\prime};{\delta}$

By (12), (4), (5), and determinism of operational semantics:

    1. (12)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\};{\delta}$

By (4), (5), and (13)

    1. (14)

${{\delta}_{1}}\cdot{e_{1}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{2}}\mathrel{::}\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\};{\delta}$

So, by definition of logical relations, $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\}$.

∎

###### Lemma B.15 (Constant soundness).

$\Gamma\vdash c\mathrel{\sim}c\,\mathrel{::}\,\texttt{TyCon}(c)$

###### Proof.

The proof follows the same steps as Theorem B.1. ∎

###### Lemma B.16 (Selfification of constants).

If $\Gamma\vdash e\mathrel{\sim}e\,\mathrel{::}\,\\{{z}\text{:}{b}\mid{r}\\}$
then $\Gamma\vdash
x\mathrel{\sim}x\,\mathrel{::}\,\\{{z}\text{:}{b}\mid{z==_{b}x}\\}$.

###### Proof.

We fix $\delta\in\Gamma$. By hypothesis $(v_{1},v_{2})/x\in\delta$ with
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\\{{z}\text{:}{b}\mid{r}\\};{\delta}$. We
need to show that
${{\delta}_{1}}\cdot{x}\mathrel{\sim}{{\delta}_{2}}\cdot{x}\mathrel{::}\\{{z}\text{:}{b}\mid{z==_{b}x}\\};{\delta}$.
Which reduces to
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\\{{z}\text{:}{b}\mid{z==_{b}x}\\};{\delta}$.
By the definition on the logical relation on basic values, we know
$v_{1}=v_{2}=c$ and $\vdash_{B}c\,\mathrel{::}\,b$. Thus, we are left to prove
that ${\delta_{1}}\cdot{((z==_{b}x)[c/z])}\hookrightarrow^{*}\texttt{true}$
and ${\delta_{2}}\cdot{((z==_{b}x)[c/z])}\hookrightarrow^{*}\texttt{true}$
which, both, trivially hold by the definition of $==_{b}$. ∎

###### Lemma B.17 (Variable soundness).

If $x:\tau\in\Gamma$, then $\Gamma\vdash
x\mathrel{\sim}x\,\mathrel{::}\,\tau$.

###### Proof.

By the definition of the logical relation it suffices to show that
$\forall\delta\in\Gamma.\delta_{1}(x)\mathrel{\sim}\delta_{2}(x)\mathrel{::}\tau;{\delta}$;
which is trivially true by the definition of $\delta\in\Gamma$. ∎

###### Lemma B.18 (Transitivity of Evaluation).

If $e\hookrightarrow^{*}e^{\prime}$, then $e\hookrightarrow^{*}v$ iff
$e^{\prime}\hookrightarrow^{*}v$.

###### Proof.

Assume $e\hookrightarrow^{*}v$. Since the $\hookrightarrow$ is by definition
deterministic, there exists a unique sequence $e\hookrightarrow
e_{1}\hookrightarrow\dots\hookrightarrow
e_{i}\hookrightarrow\dots\hookrightarrow v$. By assumption,
$e\hookrightarrow^{*}e^{\prime}$, so there exists a $j$, so $e^{\prime}\equiv
e_{j}$, and $e^{\prime}\hookrightarrow^{*}v$ following the same sequence.

Assume $e^{\prime}\hookrightarrow^{*}v$. Then
$e\hookrightarrow^{*}e^{\prime}\hookrightarrow^{*}v$ uniquely evaluates $e$ to
$v$. ∎

###### Lemma B.19 (LR closed under evaluation).

If $e_{1}\hookrightarrow^{*}e^{\prime}_{1}$,
$e_{2}\hookrightarrow^{*}e^{\prime}_{2}$, then
$e^{\prime}_{1}\mathrel{\sim}e^{\prime}_{2}\mathrel{::}\tau;{\delta}$ iff
$e_{1}\mathrel{\sim}e_{2}\mathrel{::}\tau;{\delta}$.

###### Proof.

Assume $e^{\prime}_{1}\mathrel{\sim}e^{\prime}_{2}\mathrel{::}\tau;{\delta}$,
by the definition of the logical relation on closed terms we have
$e^{\prime}_{1}\hookrightarrow^{*}v_{1}$,
$e^{\prime}_{2}\hookrightarrow^{*}v_{2}$, and
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta}$. By Lemma B.18 and by
assumption, $e_{1}\hookrightarrow^{*}e^{\prime}_{1}$ and
$e_{2}\hookrightarrow^{*}e^{\prime}_{2}$, we have
$e_{1}\hookrightarrow^{*}v_{1}$ and $e_{2}\hookrightarrow^{*}v_{2}$. By which
and $v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta}$ we get that
$e_{1}\mathrel{\sim}e_{2}\mathrel{::}\tau;{\delta}$. The other direction is
identical. ∎

###### Lemma B.20 (LR closed under parallel reduction).

If $e_{1}\rightrightarrows^{*}e^{\prime}_{1}$,
$e_{2}\rightrightarrows^{*}e^{\prime}_{2}$, and
$e^{\prime}_{1}\mathrel{\sim}e^{\prime}_{2}\mathrel{::}\tau;{\delta}$, then
$e_{1}\mathrel{\sim}e_{2}\mathrel{::}\tau;{\delta}$.

###### Proof.

By induction on $\tau$, using parallel reduction as a backward simulation
(Corollary C.15). ∎

###### Lemma B.21 (LR Compositionality).

If ${\delta_{1}}\cdot{e_{x}}\hookrightarrow^{*}v_{x_{1}}$,
${\delta_{2}}\cdot{e_{x}}\hookrightarrow^{*}v_{x_{2}}$,
$e_{1}\mathrel{\sim}e_{2}\mathrel{::}\tau;{\delta,(v_{x_{1}},v_{x_{2}})/x}$,
then $e_{1}\mathrel{\sim}e_{2}\mathrel{::}\tau[e_{x}/x];{\delta}$.

###### Proof.

By the assumption we have that

  1. (1)

${\delta_{1}}\cdot{e_{x}}\hookrightarrow^{*}v_{x_{1}}$

  2. (2)

${\delta_{2}}\cdot{e_{x}}\hookrightarrow^{*}v_{x_{2}}$

  3. (3)

$e_{1}\hookrightarrow^{*}v_{1}$

  4. (4)

$e_{2}\hookrightarrow^{*}v_{2}$

  5. (5)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta,(v_{x1},v_{x_{2}})/x}$

and we need to prove that
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau[e_{x}/x];{\delta}$. The proof goes
by structural induction on the type $\tau$.

  * •

$\tau\doteq\\{{z}\text{:}{b}\mid{r}\\}$. For $i=1,2$ we need to show that if
${\delta_{i},[v_{x_{i}}/x]}\cdot{r[v_{i}/z]}\hookrightarrow^{*}\texttt{true}$
then ${\delta_{i}}\cdot{r[v_{i}/z][e_{i}/x]}\hookrightarrow^{*}\texttt{true}$.
We have
${\delta_{i},[v_{x_{i}}/x]}\cdot{r[v_{i}/z]}\rightrightarrows^{*}{\delta_{i}}\cdot{r[v_{i}/z][e_{i}/x]}$
because substituting parallel reducing terms parallel reduces (Corollary C.3)
and parallel reduction subsumes reduction (Lemma C.4). By cotermination at
constants (Corollary C.17), we have
${\delta_{i}}\cdot{r[v_{i}/z][e_{i}/x]}\hookrightarrow^{*}\texttt{true}$.

  * •

$\tau\doteq{y}\text{:}{\tau^{\prime}_{y}}\rightarrow\tau^{\prime}$. We need to
show that if
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}{y}\text{:}{\tau^{\prime}_{y}}\rightarrow\tau^{\prime};{\delta,(v_{x_{1}},v_{x_{2}})/x}$,
then
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}{y}\text{:}{\tau^{\prime}_{y}}\rightarrow\tau^{\prime}[e_{x}/x];{\delta}$.

We fix $v_{y_{1}}$ and $v_{y_{2}}$ so that
$v_{y_{1}}\mathrel{\sim}v_{y_{2}}\mathrel{::}\tau^{\prime}_{y};{\delta,(v_{x_{1}},v_{x_{2}})/x}$.

Then, we have that $v_{1}\ v_{y_{1}}\mathrel{\sim}v_{2}\
v_{y_{2}}\mathrel{::}\tau^{\prime};{\delta,(v_{x_{1}},v_{x_{2}})/x,(v_{y_{1}},v_{y_{2}})/y}$.

By inductive hypothesis, we have that $v_{1}\ v_{y_{1}}\mathrel{\sim}v_{2}\
v_{y_{2}}\mathrel{::}\tau^{\prime}[e_{x}/x];{\delta,(v_{y_{1}},v_{y_{2}})/y}$.

By inductive hypothesis on the fixed arguments, we also get
$v_{y_{1}}\mathrel{\sim}v_{y_{2}}\mathrel{::}\tau^{\prime}_{y}[e_{x}/x];{\delta}$.

Combined, we get
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}{y}\text{:}{\tau^{\prime}_{y}}\rightarrow\tau^{\prime}[e_{x}/x];{\delta}$.

  * •

$\tau\doteq\texttt{PEq}_{\tau^{\prime}}\ \\{e_{l}\\}\ \\{e_{r}\\}$. We need to
show that if
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\};{\delta,(v_{x_{1}},v_{x_{2}})/x}$, then
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\}[e_{x}/x];{\delta}$.

This reduces to showing that if
${\delta_{1},[v_{x_{1}}/x]}\cdot{e_{l}}\mathrel{\sim}{\delta_{2},[v_{x_{2}}/x]}\cdot{e_{r}}\mathrel{::}\tau^{\prime};{\delta}$,
then
${\delta_{1}}\cdot{e_{l}[e_{x}/x]}\mathrel{\sim}{\delta_{2}}\cdot{e_{r}[e_{x}/x]}\mathrel{::}\tau^{\prime};{\delta}$;
we find
${\delta_{1}}\cdot{e_{l}[e_{x}/x]}\rightrightarrows^{*}{\delta_{1},[v_{x_{1}}/x]}\cdot{e_{l}}$
and
${\delta_{2}}\cdot{e_{r}[e_{x}/x]}\rightrightarrows^{*}{\delta_{2},[v_{x_{2}}/x]}\cdot{e_{r}}$
because substituting multiple parallel reduction is parallel reduction
(Corollary C.3). The logical relation is closed under parallel reduction
(Lemma B.20), and so
${\delta_{1}}\cdot{e_{l}[e_{x}/x]}\mathrel{\sim}{\delta_{2}}\cdot{e_{r}[e_{x}/x]}\mathrel{::}\tau^{\prime};{\delta}$.

∎

###### Theorem B.22 (LR Fundamental Property).

If $\Gamma\vdash e\mathrel{\text{::}}\tau$, then $\Gamma\vdash
e\mathrel{\sim}e\,\mathrel{::}\,\tau$.

###### Proof.

The proof goes by induction on the derivation tree:

  * TSub

By inversion of the rule we have

    1. (1)

$\Gamma\vdash e\mathrel{\text{::}}\tau^{\prime}$

    2. (2)

${\Gamma}\vdash{\tau^{\prime}}\ \preceq\ {\tau}$

By IH on (1) we have

    1. (3)

$\Gamma\vdash e\mathrel{\sim}e\,\mathrel{::}\,\tau^{\prime}$

By (3), (4), and Lemma B.14 we have $\Gamma\vdash
e\mathrel{\sim}e\,\mathrel{::}\,\tau$.

  * TCon

By Lemma B.15.

  * TSelf

By inversion of the rule, we have:

    1. (1)

$\Gamma\vdash e\mathrel{\text{::}}\\{{z}\text{:}{b}\mid{r}\\}$.

    2. (2)

By the IH on (1), we have:

$\Gamma\vdash e\mathrel{\sim}e\,\mathrel{::}\,\\{{z}\text{:}{b}\mid{r}\\}$.

    3. (3)

We fix a $\delta$ such that:

$\delta\in\Gamma$ and

${\delta_{1}}\cdot{e}\mathrel{\sim}{\delta_{2}}\cdot{e}\mathrel{::}\\{{z}\text{:}{b}\mid{r}\\};{\delta}$

    4. (4)

There must exist $v_{1}$ and $v_{2}$ such that:

${\delta_{1}}\cdot{e}\hookrightarrow^{*}v_{1}$

${\delta_{2}}\cdot{e}\hookrightarrow^{*}v_{2}$

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\\{{z}\text{:}{b}\mid{r}\\};{\delta}$

    5. (5)

By definition, $v_{1}=v_{2}=c$ such that:

$\vdash_{B}c\,\mathrel{::}\,b$

${\delta_{1}}\cdot{r[c/x]}\hookrightarrow^{*}\texttt{true}$

${\delta_{2}}\cdot{r[c/x]}\hookrightarrow^{*}\texttt{true}$

    6. (6)

We find
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\\{{z}\text{:}{b}\mid{z==_{b}e}\\};{\delta}$,
because:

$\vdash_{B}c\,\mathrel{::}\,b$ by (5)

${\delta_{1}}\cdot{(z==_{b}e)[c/z]}\hookrightarrow^{*}\texttt{true}$ because
${\delta_{1}}\cdot{e}\hookrightarrow^{*}v_{1}=c$ by (4)

${\delta_{2}}\cdot{(z==_{b}e)[c/z]}\hookrightarrow^{*}\texttt{true}$ because
${\delta_{2}}\cdot{e}\hookrightarrow^{*}v_{2}=c$ by (4)

  * TVar

By inversion of the rule and Lemma B.17.

  * TLam

By hypothesis:

    1. (1)

$\Gamma\vdash\lambda
x\mathord{:}\tau_{x}.~{}e\mathrel{\text{::}}{x}\text{:}{\tau_{x}}\rightarrow\tau$

By inversion of the rule we have

    1. (2)

$\Gamma,x:\tau_{x}\vdash e\mathrel{\text{::}}\tau$

    2. (3)

$\Gamma\vdash\tau_{x}$

By inductive hypothesis on (2) we have

    1. (4)

$\Gamma,x:\tau_{x}\vdash e\mathrel{\sim}e\,\mathrel{::}\,\tau$

We fix a $\delta$, $v_{x_{1}}$, and $v_{x_{2}}$ so that

    1. (5)

$\delta\in\Gamma$

    2. (6)

$v_{x_{1}}\mathrel{\sim}v_{x_{2}}\mathrel{::}\tau_{x};{\delta}$

Let $\delta^{\prime}\doteq\delta,(v_{x_{1}},v_{x_{2}})/x$.

By the definition of the logical relation on open terms, (4), (5), and (6) we
have

    1. (7)

${{\delta^{\prime}}_{1}}\cdot{e}\mathrel{\sim}{{\delta^{\prime}}_{2}}\cdot{e}\mathrel{::}\tau;{\delta^{\prime}}$

By the definition of substitution

    1. (8)

${\delta_{1}}\cdot{e[v_{x_{1}}/x]}\mathrel{\sim}{\delta_{2}}\cdot{e[v_{x_{2}}/x]}\mathrel{::}\tau;{\delta^{\prime}}$

By the definition of the logical relation on closed expressions

    1. (9)

${\delta_{1}}\cdot{e[v_{x_{1}}/x]}\hookrightarrow^{*}v_{1}$,
${\delta_{2}}\cdot{e[v_{x_{2}}/x]}\hookrightarrow^{*}v_{2}$, and
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta^{\prime}}$

By the definition and determinism of operational semantics

    1. (10)

${\delta_{1}}\cdot{(\lambda x\mathord{:}\tau_{x}.~{}e)\
v_{x_{1}}}\hookrightarrow^{*}v_{1}$, ${\delta_{2}}\cdot{(\lambda
x\mathord{:}\tau_{x}.~{}e)\ v_{x_{2}}}\hookrightarrow^{*}v_{2}$, and
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta^{\prime}}$

By (6) and the definition of logical relation on function values,

    1. (11)

${{\delta}_{1}}\cdot{\lambda
x\mathord{:}\tau_{x}.~{}e}\mathrel{\sim}{{\delta}_{2}}\cdot{\lambda
x\mathord{:}\tau_{x}.~{}e}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

Thus, by the definition of the logical relation, $\Gamma\vdash\lambda
x\mathord{:}\tau_{x}.~{}e\mathrel{\sim}\lambda
x\mathord{:}\tau_{x}.~{}e\,\mathrel{::}\,{x}\text{:}{\tau_{x}}\rightarrow\tau$

  * TApp

By hypothesis:

    1. (1)

$\Gamma\vdash e\ e_{x}\mathrel{\text{::}}\tau[e_{x}/x]$

By inversion we get

    1. (2)

$\Gamma\vdash e\mathrel{\text{::}}{x}\text{:}{\tau_{x}}\rightarrow\tau$

    2. (3)

$\Gamma\vdash e_{x}\mathrel{\text{::}}\tau_{x}$

By inductive hypothesis

    1. (3)

$\Gamma\vdash
e\mathrel{\sim}e\,\mathrel{::}\,{x}\text{:}{\tau_{x}}\rightarrow\tau$

    2. (4)

$\Gamma\vdash e_{x}\mathrel{\sim}e_{x}\,\mathrel{::}\,\tau_{x}$

We fix a $\delta\in\Gamma$. Then, by the definition of the logical relation on
open terms

    1. (5)

${{\delta}_{1}}\cdot{e}\mathrel{\sim}{{\delta}_{2}}\cdot{e}\mathrel{::}({x}\text{:}{\tau_{x}}\rightarrow\tau);{\delta}$

    2. (6)

${{\delta}_{1}}\cdot{e_{x}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{x}}\mathrel{::}\tau_{x};{\delta}$

By the definition of the logical relation on open terms:

    1. (7)

${\delta_{1}}\cdot{e}\hookrightarrow^{*}v_{1}$

    2. (8)

${\delta_{2}}\cdot{e}\hookrightarrow^{*}v_{2}$

    3. (9)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

    4. (10)

${\delta_{1}}\cdot{e_{x}}\hookrightarrow^{*}v_{x_{1}}$

    5. (11)

${\delta_{2}}\cdot{e_{x}}\hookrightarrow^{*}v_{x_{2}}$

    6. (12)

$v_{x_{1}}\mathrel{\sim}v_{x_{2}}\mathrel{::}\tau_{x};{\delta}$

By (7) and (10)

    1. (13)

${\delta_{1}}\cdot{e\ e_{x}}\hookrightarrow^{*}v_{1}\ v_{x_{1}}$

By (8) and (11)

    1. (14)

${\delta_{2}}\cdot{e\ e_{x}}\hookrightarrow^{*}v_{2}\ v_{x_{2}}$

By (9), (12), and the definition of logical relation on functions:

    1. (15)

$v_{1}\ v_{x_{1}}\mathrel{\sim}v_{2}\
v_{x_{2}}\mathrel{::}\tau;{\delta,(v_{x_{1}},v_{x_{2}})/x}$

By (13), (14), (15), and Lemma B.19

    1. (16)

${\delta_{1}}\cdot{e\ e_{x}}\mathrel{\sim}{\delta_{2}}\cdot{e\
e_{x}}\mathrel{::}\tau;{\delta,(v_{x_{1}},v_{x_{2}})/x}$

By (10), (11), (16), and Lemma B.21

    1. (17)

${\delta_{1}}\cdot{e\ e_{x}}\mathrel{\sim}{\delta_{2}}\cdot{e\
e_{x}}\mathrel{::}\tau[e_{x}/x];{\delta}$

So from the definition of logical relations, $\Gamma\vdash e\
e_{x}\mathrel{\sim}e\ e_{x}\,\mathrel{::}\,\tau[e_{x}/x]$.

  * TEqBase

By hypothesis:

    1. (1)

$\Gamma\vdash\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e\mathrel{\text{::}}\texttt{PEq}_{b}\ \\{e_{l}\\}\ \\{e_{r}\\}$

By inversion of the rule:

    1. (2)

$\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{r}$

    2. (3)

$\Gamma\vdash e_{r}\mathrel{\text{::}}\tau_{l}$

    3. (4)

${\Gamma}\vdash{\tau_{r}}\ \preceq\ {b}$

    4. (5)

${\Gamma}\vdash{\tau_{l}}\ \preceq\ {b}$

    5. (6)

$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
e\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$

By inductive hypothesis on (2), (3), and (6) we have

    1. (7)

$\Gamma\vdash e_{l}\mathrel{\sim}e_{l}\,\mathrel{::}\,\tau_{r}$

    2. (8)

$\Gamma\vdash e_{r}\mathrel{\sim}e_{r}\,\mathrel{::}\,\tau_{l}$

    3. (9)

$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
e\mathrel{\sim}e\,\mathrel{::}\,\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$

We fix $\delta\in\Gamma$. Then (7) and (8) become

    1. (10)

${{\delta}_{1}}\cdot{e_{l}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{l}}\mathrel{::}\tau_{r};{\delta}$

    2. (11)

${{\delta}_{1}}\cdot{e_{r}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{r}}\mathrel{::}\tau_{l};{\delta}$

By the definition of the logical relation on closed terms:

    1. (12)

${\delta_{1}}\cdot{e_{l}}\hookrightarrow^{*}v_{l_{1}}$

    2. (13)

${\delta_{2}}\cdot{e_{l}}\hookrightarrow^{*}v_{l_{2}}$

    3. (14)

$v_{l_{1}}\mathrel{\sim}v_{l_{2}}\mathrel{::}\tau_{l};{\delta}$

    4. (15)

${\delta_{1}}\cdot{e_{r}}\hookrightarrow^{*}v_{r_{1}}$

    5. (16)

${\delta_{2}}\cdot{e_{r}}\hookrightarrow^{*}v_{r_{2}}$

    6. (17)

$v_{r_{1}}\mathrel{\sim}v_{r_{2}}\mathrel{::}\tau_{r};{\delta}$

We define
$\delta^{\prime}\doteq\delta,(v_{r_{1}},v_{r_{2}})/r,(v_{l_{1}},v_{l_{2}})/l$.

By (9), (14), and (17) we have

    1. (18)

${{\delta^{\prime}}_{1}}\cdot{e}\mathrel{\sim}{{\delta^{\prime}}_{2}}\cdot{e}\mathrel{::}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\};{\delta^{\prime}}$

By the definition of the logical relation on closed terms:

    1. (19)

${\delta^{\prime}}\cdot{e}\hookrightarrow^{*}v_{1}$

    2. (20)

${\delta^{\prime}}\cdot{e}\hookrightarrow^{*}v_{2}$

    3. (21)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\};{\delta^{\prime}}$

By (21) and the definition of logical relation on basic values:

    1. (19)

${\delta^{\prime}_{1}}\cdot{(l==_{b}r})\hookrightarrow^{*}\texttt{true}$

    2. (20)

${\delta^{\prime}_{2}}\cdot{(l==_{b}r})\hookrightarrow^{*}\texttt{true}$

By the definition of $==_{b}$

    1. (21)

$v_{l_{1}}=v_{r_{1}}$

    2. (22)

$v_{l_{2}}=v_{r_{2}}$

By (14) and (17) and since $\tau_{l}$ and $\tau_{r}$ are basic types

    1. (23)

$v_{l_{1}}=v_{l_{2}}$

    2. (24)

$v_{r_{1}}=v_{r_{2}}$

By (21) and (24)

    1. (25)

$v_{l_{1}}=v_{r_{2}}$

By the definition of the logical relation on basic types

    1. (26)

$v_{l_{1}}\mathrel{\sim}v_{r_{2}}\mathrel{::}b;{\delta}$

By which, (12), (16), and Lemma B.19

    1. (27)

${\delta_{1}}\cdot{e_{l}}\mathrel{\sim}{\delta_{2}}\cdot{e_{r}}\mathrel{::}b;{\delta}$

By (12), (15), and (19)

    1. (28)

${\delta_{1}}\cdot{\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e}\hookrightarrow^{*}\texttt{bEq}_{b}\ v_{l_{1}}\ v_{r_{1}}\ v_{1}$

By (13), (16), and (20)

    1. (29)

${\delta_{2}}\cdot{\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e}\hookrightarrow^{*}\texttt{bEq}_{b}\ v_{l_{2}}\ v_{r_{2}}\ v_{2}$

By (27) and the definition of the logical relation on EqRT

    1. (30)

$\texttt{bEq}_{b}\ v_{l_{1}}\ v_{r_{1}}\ v_{1}\mathrel{\sim}\texttt{bEq}_{b}\
v_{l_{2}}\ v_{r_{2}}\ v_{2}\mathrel{::}\texttt{PEq}_{b}\ \\{e_{l}\\}\
\\{e_{r}\\};{\delta}$.

By (28), (29), and (30)

    1. (31)

${{\delta}_{1}}\cdot{\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e}\mathrel{\sim}{{\delta}_{2}}\cdot{\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e}\mathrel{::}\texttt{PEq}_{b}\ \\{e_{l}\\}\ \\{e_{r}\\};{\delta}$.

So, by the definition on the logical relation, $\Gamma\vdash\texttt{bEq}_{b}\
e_{l}\ e_{r}\ e\mathrel{\sim}\texttt{bEq}_{b}\ e_{l}\ e_{r}\
e\,\mathrel{::}\,\texttt{PEq}_{b}\ \\{e_{l}\\}\ \\{e_{r}\\}$.

  * TEqFun

By hypothesis

    1. (1)

$\Gamma\vdash\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\ }e_{l}\ e_{r}\
e\mathrel{\text{::}}\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}$

By inversion of the rule

    1. (2)

$\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{r}$

    2. (3)

$\Gamma\vdash e_{r}\mathrel{\text{::}}\tau_{l}$

    3. (4)

${\Gamma}\vdash{\tau_{r}}\ \preceq\ {{x}\text{:}{\tau_{x}}\rightarrow\tau}$

    4. (5)

${\Gamma}\vdash{\tau_{l}}\ \preceq\ {{x}\text{:}{\tau_{x}}\rightarrow\tau}$

    5. (6)

$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
e\mathrel{\text{::}}({x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\
\\{l\ x\\}\ \\{r\ x\\})$

    6. (7)

$\Gamma\vdash{x}\text{:}{\tau_{x}}\rightarrow\tau$

By inductive hypothesis on (2), (3), and (6) we have

    1. (8)

$\Gamma\vdash e_{l}\mathrel{\sim}e_{l}\,\mathrel{::}\,\tau_{r}$

    2. (9)

$\Gamma\vdash e_{r}\mathrel{\sim}e_{r}\,\mathrel{::}\,\tau_{l}$

    3. (10)

$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
e\mathrel{\sim}e\,\mathrel{::}\,({x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\
\\{l\ x\\}\ \\{r\ x\\})$

By (8), (9), and Lemma B.14

    1. (11)

$\Gamma\vdash
e_{l}\mathrel{\sim}e_{l}\,\mathrel{::}\,{x}\text{:}{\tau_{x}}\rightarrow\tau$

    2. (12)

$\Gamma\vdash
e_{r}\mathrel{\sim}e_{r}\,\mathrel{::}\,{x}\text{:}{\tau_{x}}\rightarrow\tau$

We fix $\delta\in\Gamma$. Then (11), and (12) become

    1. (13)

${{\delta}_{1}}\cdot{e_{l}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{l}}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

    2. (14)

${{\delta}_{1}}\cdot{e_{r}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{r}}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

By the definition of the logical relation on closed terms:

    1. (15)

${\delta_{1}}\cdot{e_{l}}\hookrightarrow^{*}v_{l_{1}}$

    2. (16)

${\delta_{2}}\cdot{e_{l}}\hookrightarrow^{*}v_{l_{2}}$

    3. (17)

$v_{l_{1}}\mathrel{\sim}v_{l_{2}}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

    4. (18)

$v_{l_{1}}\mathrel{\sim}v_{l_{2}}\mathrel{::}\tau_{l};{\delta}$

    5. (19)

${\delta_{1}}\cdot{e_{r}}\hookrightarrow^{*}v_{r_{1}}$

    6. (20)

${\delta_{2}}\cdot{e_{r}}\hookrightarrow^{*}v_{r_{2}}$

    7. (21)

$v_{r_{1}}\mathrel{\sim}v_{r_{2}}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

    8. (22)

$v_{r_{1}}\mathrel{\sim}v_{r_{2}}\mathrel{::}\tau_{r};{\delta}$

We fix $v_{x_{1}}$ and $v_{x_{2}}$ so that
$v_{x_{1}}\mathrel{\sim}v_{x_{2}}\mathrel{::}\tau_{x};{\delta}$. Let
$\delta_{x}\doteq\delta,(v_{x_{1}},v_{x_{2}})/x$.

By the definition on the logical relation on function values, (17) and (21)
become

    1. (23)

$v_{l_{1}}\ v_{x_{1}}\mathrel{\sim}v_{l_{2}}\
v_{x_{2}}\mathrel{::}\tau;{\delta_{x}}$

    2. (24)

$v_{r_{1}}\ v_{x_{1}}\mathrel{\sim}v_{r_{2}}\
v_{x_{2}}\mathrel{::}\tau;{\delta_{x}}$

Let $\delta_{lr}\doteq\delta,(v_{r_{1}},v_{r_{2}})/r,(v_{l_{1}},v_{l_{2}})/l$.

By the definition of the logical relation on closed terms, (10) becomes:

    1. (25)

${\delta_{lr}}\cdot{e}\hookrightarrow^{*}v_{1}$

    2. (26)

${\delta_{lr}}\cdot{e}\hookrightarrow^{*}v_{2}$

    3. (27)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\
\\{l\ x\\}\ \\{r\ x\\};{\delta_{lr}}$

By (27) and the definition of logical relation on function values:

    1. (28)

$v_{1}\ v_{x_{1}}\mathrel{\sim}v_{2}\
v_{x_{2}}\mathrel{::}\texttt{PEq}_{\tau}\ \\{l\ x\\}\ \\{r\
x\\};{\delta_{lr},(v_{x_{1}},v_{x_{2}})/x}$

By the definition of the logical relation on EqRT

    1. (29)

$v_{l_{1}}\ v_{x_{1}}\mathrel{\sim}v_{r_{2}}\
v_{x_{2}}\mathrel{::}\tau;{\delta_{lr},(v_{x_{1}},v_{x_{2}})/x}$

By the definition of logical relations on function values

    1. (30)

$v_{l_{1}}\mathrel{\sim}v_{r_{2}}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta_{lr}}$

By (7), $l$ and $r$ do not appear free in the relation, so

    1. (31)

$v_{l_{1}}\mathrel{\sim}v_{r_{2}}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

By which, (15), (20), and Lemma B.19

    1. (32)

${\delta_{1}}\cdot{e_{l}}\mathrel{\sim}{\delta_{2}}\cdot{e_{r}}\mathrel{::}{x}\text{:}{\tau_{x}}\rightarrow\tau;{\delta}$

By (15), (19), and (25)

    1. (33)

${\delta_{1}}\cdot{\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\ }e_{l}\
e_{r}\ e}\hookrightarrow^{*}\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\
}v_{l_{1}}\ v_{r_{1}}\ v_{1}$

By (16), (20), and (26)

    1. (34)

${\delta_{2}}\cdot{\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\ }e_{l}\
e_{r}\ e}\hookrightarrow^{*}\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\
}v_{l_{2}}\ v_{r_{2}}\ v_{2}$

By (32) and the definition of the logical relation on EqRT

    1. (35)

$\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\ }v_{l_{1}}\ v_{r_{1}}\
v_{1}\mathrel{\sim}\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\
}v_{l_{2}}\ v_{r_{2}}\
v_{2}\mathrel{::}\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\};{\delta}$.

By (33), (34), and (35)

    1. (36)

${{\delta}_{1}}\cdot{\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\
}e_{l}\ e_{r}\
e}\mathrel{\sim}{{\delta}_{2}}\cdot{\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\
}e_{l}\ e_{r}\
e}\mathrel{::}\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\};{\delta}$.

So, by the definition on the logical relation,
$\Gamma\vdash\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\ }e_{l}\ e_{r}\
e\mathrel{\sim}\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\ }e_{l}\
e_{r}\ e\,\mathrel{::}\,\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
\\{e_{l}\\}\ \\{e_{r}\\}$.

∎

###  B.5. The Logical Relation and the $\mathsf{EqRT}$ Type are Equivalence
Relations

###### Theorem B.23 (The logical relation is an equivalence relation).

$\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$ is reflexive,
symmetric, and transivite.

  * •

Reflexivity: If $\Gamma\vdash e\mathrel{\text{::}}\tau$, then $\Gamma\vdash
e\mathrel{\sim}e\,\mathrel{::}\,\tau$.

  * •

Symmetry: If $\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$, then
$\Gamma\vdash e_{2}\mathrel{\sim}e_{1}\,\mathrel{::}\,\tau$.

  * •

Transitivity: If $\Gamma\vdash e_{2}\mathrel{\text{::}}\tau$ and $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$ and $\Gamma\vdash
e_{2}\mathrel{\sim}e_{3}\,\mathrel{::}\,\tau$, then $\Gamma\vdash
e_{1}\mathrel{\sim}e_{3}\,\mathrel{::}\,\tau$.

###### Proof.

Reflexivity: This is exactly the Fundamental Property B.22.

Symmetry: Let $\bar{\delta}$ be defined such that
$\bar{\delta}_{1}(x)=\delta_{2}(x)$ and $\bar{\delta}_{2}(x)=\delta_{1}(x)$.
First, we prove that $v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta}$
implies $v_{2}\mathrel{\sim}v_{1}\mathrel{::}\tau;{\bar{\delta}}$, by
structural induction on $\tau$.

  * •

$\tau\doteq\\{{z}\text{:}{b}\mid{r}\\}$. This case is immediate: we have to
show that
$c\mathrel{\sim}c\mathrel{::}\\{{z}\text{:}{b}\mid{r}\\};{\bar{\delta}}$ given
$c\mathrel{\sim}c\mathrel{::}\\{{z}\text{:}{b}\mid{r}\\};{\delta}$. But the
definition in this case is itself symmetric: the predicate goes to true under
both substitutions.

  * •

$\tau\doteq{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}$. We fix
$v_{x_{1}}$ and $v_{x_{2}}$ so that

    1. (1)

$v_{x_{1}}\mathrel{\sim}v_{x_{2}}\mathrel{::}\tau^{\prime}_{x};{\delta}$

By the definition of logical relations on open terms and inductive hypothesis

    1. (2)

$v_{x_{2}}\mathrel{\sim}v_{x_{1}}\mathrel{::}\tau^{\prime}_{x};{\bar{\delta}}$

By the definition on logical relations on functions

    1. (3)

$v_{1}\ v_{x_{1}}\mathrel{\sim}v_{2}\
v_{x_{2}}\mathrel{::}\tau^{\prime};{\delta,(v_{x_{1}},v_{x_{2}})/x}$

By the definition of logical relations on open terms and since the expressions
$v_{1}\ v_{x_{1}}$ and $v_{2}\ v_{x_{2}}$ are closed, By the inductive
hypothesis on $\tau^{\prime}$:

    1. (4)

$v_{2}\ v_{x_{2}}\mathrel{\sim}v_{1}\
v_{x_{1}}\mathrel{::}\tau^{\prime};{\bar{\delta},x:\tau^{\prime}_{x}}$

By (2) and the definition of logical relations on open terms

    1. (5)

$v_{2}\ v_{x_{2}}\mathrel{\sim}v_{1}\
v_{x_{1}}\mathrel{::}\tau^{\prime};{\bar{\delta},(v_{x_{2}},v_{x_{1}})/x}$

By the definition of the logical relation on functions, we conclude that
$v_{2}\mathrel{\sim}v_{1}\mathrel{::}{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime};{\bar{\delta}}$

  * •

$\tau\doteq\texttt{PEq}_{\tau^{\prime}}\ \\{e_{l}\\}\ \\{e_{r}\\}$. By
assumption,

    1. (1)

$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\};{\delta}$

By the definition of the logical relation on EqRT types

    1. (2)

${\delta_{1}}\cdot{e_{l}}\mathrel{\sim}{\delta_{2}}\cdot{e_{r}}\mathrel{::}\tau^{\prime};{\delta}$

i.e., ${\delta_{1}}\cdot{(}e_{l})\hookrightarrow^{*}v_{l}$ and similarly for
$v_{r}$ such that
$v_{l}\mathrel{\sim}v_{r}\mathrel{::}\tau^{\prime};{\delta}$.

By the IH on $\tau^{\prime}$, we have:

    1. (3)

$v_{r}\mathrel{\sim}v_{l}\mathrel{::}\tau^{\prime};{\bar{\delta}}$

And so, by the definition of the LR on equality proofs:

    1. (4)

$v_{2}\mathrel{\sim}v_{1}\mathrel{::}\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}\\}\ \\{e_{r}\\};{\bar{\delta}}$

Next, we show that $\delta\in\Gamma$ implies $\bar{\delta}\in\Gamma$. We go by
structural induction on $\Gamma$.

  * •

$\Gamma=\cdot$. This case is trivial.

  * •

$\Gamma=\Gamma^{\prime},x:\tau$. For $x:\tau$, we know that
$\delta_{1}(x)\mathrel{\sim}\delta_{2}(x)\mathrel{::}\tau;{\delta}$. By the IH
on $\tau$, we find
$\delta_{2}(x)\mathrel{\sim}\delta_{1}(x)\mathrel{::}\tau;{\bar{\delta}}$,
which is just the same as
$\bar{\delta}_{1}(x)\mathrel{\sim}\bar{\delta}_{2}(x)\mathrel{::}\tau;{\bar{\delta}}$.
By the IH on $\Gamma^{\prime}$, we can use similar reasoning to find
$\bar{\delta}_{1}(y)\mathrel{\sim}\bar{\delta}_{2}(y)\mathrel{::}\tau^{\prime};{\bar{\delta}}$
for all $y:\tau^{\prime}\in\Gamma^{\prime}$.

Now, suppose $\Gamma\vdash e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$; we
must show $\Gamma\vdash e_{2}\mathrel{\sim}e_{1}\,\mathrel{::}\,\tau$. We fix
$\delta\in\Gamma$; we must show
${{\delta}_{1}}\cdot{e_{2}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{1}}\mathrel{::}\tau;{\delta}$,
i.e., there must exist $v_{1}$ and $v_{2}$ such that
${\delta_{1}}\cdot{e_{2}}\hookrightarrow^{*}v_{2}$ and
${\delta_{2}}\cdot{e_{1}}\hookrightarrow^{*}v_{1}$ and
$v_{2}\mathrel{\sim}v_{1}\mathrel{::}\tau;{\delta}$. We have
$\delta\in\Gamma$, and so $\bar{\delta}\in\Gamma$ by our second lemma. But
then, by assumption, we have $v_{1}$ and $v_{2}$ such that
${\bar{\delta_{1}}}\cdot{e_{1}}\hookrightarrow^{*}v_{1}$ and
${\bar{\delta_{2}}}\cdot{e_{2}}\hookrightarrow^{*}v_{2}$ and
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\bar{\delta}}$. Our first lemma
then yields $v_{2}\mathrel{\sim}v_{1}\mathrel{::}\tau;{\delta}$ as desired.

Transitivity: First, we prove an inner property: if $\delta\in\Gamma$ and
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta}$ and
$v_{2}\mathrel{\sim}v_{3}\mathrel{::}\tau;{\delta}$, then
$v_{1}\mathrel{\sim}v_{3}\mathrel{::}\tau;{\delta}$. We go by structural
induction on the type index $\tau$.

  * •

$\tau\doteq\\{{z}\text{:}{b}\mid{r}\\}$. Here all of the values must be the
fixed constant $c$. Furthermore, we must have
${\delta_{1}}\cdot{r[c/x]}\hookrightarrow^{*}\texttt{true}$ and
${\delta_{2}}\cdot{r[c/x]}\hookrightarrow^{*}\texttt{true}$, so we can
immediately find $v_{1}\mathrel{\sim}v_{3}\mathrel{::}\tau;{\delta}$.

  * •

$\tau\doteq{x}\text{:}{\tau^{\prime}_{x}}\rightarrow\tau^{\prime}$.

Let $v_{l}\mathrel{\sim}v_{r}\mathrel{::}\tau^{\prime}_{x};{\delta}$ be given.
We must show that
$v_{1}\mathrel{\sim}v_{3}\mathrel{::}\tau;{\delta,(v_{l},v_{r})/x}$. We know
by assumption that: $v_{1}\ v_{l}\mathrel{\sim}v_{2}\
v_{r}\mathrel{::}\tau^{\prime};{\delta,(v_{l},v_{r})/x}$ and $v_{2}\
v_{l}\mathrel{\sim}v_{3}\
v_{r}\mathrel{::}\tau^{\prime};{\delta,(v_{l},v_{r})/x}$. By the IH on
$\tau^{\prime}$, we find $v_{1}\ v_{l}\mathrel{\sim}v_{3}\
v_{r}\mathrel{::}\tau^{\prime};{\delta,(v_{l},v_{r})/x}$; which gives
$v_{1}\mathrel{\sim}v_{3}\mathrel{::}\tau;{\delta,(v_{l},v_{r})/x}$.

  * •

$\tau\doteq\texttt{PEq}_{\tau^{\prime}}\ \\{e_{l}\\}\ \\{e_{r}\\}$.

To find $v_{1}\mathrel{\sim}v_{3}\mathrel{::}\texttt{PEq}_{\tau}\ \\{e_{l}\\}\
\\{e_{r}\\};{\delta}$, we merely need to find that
${\delta_{1}}\cdot{e_{l}}\mathrel{\sim}{\delta_{2}}\cdot{e_{r}}\mathrel{::}\tau;{\delta}$,
which we have by inversion on
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\texttt{PEq}_{\tau}\ \\{e_{l}\\}\
\\{e_{r}\\};{\delta}$.

With our proof that the value relation is transitive in hand, we turn our
attention to the open relation. Suppose $\Gamma\vdash
e_{1}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$ and $\Gamma\vdash
e_{2}\mathrel{\sim}e_{3}\,\mathrel{::}\,\tau$; we want to see $\Gamma\vdash
e_{1}\mathrel{\sim}e_{3}\,\mathrel{::}\,\tau$. Let $\delta\in\Gamma$ be given.
We have
${{\delta}_{1}}\cdot{e_{1}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{2}}\mathrel{::}\tau;{\delta}$
and
${{\delta}_{1}}\cdot{e_{2}}\mathrel{\sim}{{\delta}_{2}}\cdot{e_{3}}\mathrel{::}\tau;{\delta}$.
By the definition of the logical relations, we have
${\delta_{1}}\cdot{e_{1}}\hookrightarrow^{*}v_{1}$,
${\delta_{2}}\cdot{e_{2}}\hookrightarrow^{*}v_{2}$,
${\delta_{1}}\cdot{e_{2}}\hookrightarrow^{*}v_{2}^{\prime}$,
${\delta_{2}}\cdot{e_{3}}\hookrightarrow^{*}v_{3}$,
$v_{1}\mathrel{\sim}v_{2}\mathrel{::}\tau;{\delta}$, and
$v_{2}^{\prime}\mathrel{\sim}v_{3}\mathrel{::}\tau;{\delta}$.

Moreover, we know that $e_{2}$ is well typed, so by the fundamental theorem
(Theorem B.22), we know that $\Gamma\vdash
e_{2}\mathrel{\sim}e_{2}\,\mathrel{::}\,\tau$, and so
$v_{2}\mathrel{\sim}v_{2}^{\prime}\mathrel{::}\tau;{\delta}$.

By our transitivity lemma on the value relation, we can find that $v_{1}$ is
equivalent to $v_{2}$ is equivalent to $v_{2}^{\prime}$ is equivalent to
$v_{3}$, and so $v_{1}\mathrel{\sim}v_{3}\mathrel{::}\tau;{\delta}$.

∎

$\begin{array}[]{rcl}\mathsf{pf}&:&e\rightarrow e\rightarrow\tau\\\
\mathsf{pf}(l,r,b)&=&\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}\\\
\mathsf{pf}(l,r,{x}\text{:}{\tau_{x}}\rightarrow\tau)&=&{x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\
\\{l\ x\\}\ \\{r\ x\\}\\\ \end{array}$

Our propositional equality $\texttt{PEq}_{\tau}\ \\{e_{l}\\}\ \\{e_{r}\\}$ is
a reflection of the logical relation, so it is unsurprising that it is also an
equivalence relation. We can prove that our propositional equality is treated
as an equivalence relation by the syntactic type system. There are some tiny
wrinkles in the syntactic system: symmetry and transitivity produce normalized
proofs, but reflexivity produces unnormalized ones in order to generate the
correct invariant types $\tau_{l}$ and $\tau_{r}$ in the base case.

###### Theorem B.24 (EqRT is an equivalence relation).

$\texttt{PEq}_{\tau}\ \\{e_{1}\\}\ \\{e_{2}\\}$ is reflexive, symmetric, and
transitive on equable types. That is, for all $\tau$ that contain only
refinements and functions:

  * •

Reflexivity: If $\Gamma\vdash e\mathrel{\text{::}}\tau$, then there exists
$e_{p}$ such that $\Gamma\vdash e_{p}\mathrel{\text{::}}\texttt{PEq}_{\tau}\
\\{e\\}\ \\{e\\}$.

  * •

Symmetry: $\forall\Gamma,\tau,e_{1},e_{2},v_{12}$. if $\Gamma\vdash
v_{12}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{1}\\}\ \\{e_{2}\\}$, then
there exists $v_{21}$ such that $\Gamma\vdash
v_{21}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{2}\\}\ \\{e_{1}\\}$.

  * •

Transitivity: $\forall\Gamma,\tau,e_{1},e_{2},e_{3},v_{12},v_{23}$. if
$\Gamma\vdash v_{12}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{1}\\}\
\\{e_{2}\\}$ and $\Gamma\vdash v_{23}\mathrel{\text{::}}\texttt{PEq}_{\tau}\
\\{e_{2}\\}\ \\{e_{3}\\}$, then there exists $v_{13}$ such that $\Gamma\vdash
v_{13}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{1}\\}\ \\{e_{3}\\}$.

###### Proof.

Reflexivity: We strengthen the IH, simultaneously proving that there exist
$e_{p},e_{\mathsf{pf}}$ and ${\Gamma}\vdash{\tau_{l}}\ \preceq\ {\tau}$ and
${\Gamma}\vdash{\tau_{r}}\ \preceq\ {\tau}$ such that
$\Gamma,l:\tau_{l},r:\tau_{r}\vdash
e_{\mathsf{pf}}\mathrel{\text{::}}\mathsf{pf}(e,e,\tau)$ and $\Gamma\vdash
e_{p}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e\\}\ \\{e\\}$ by induction on
$\tau$, leaving $e$ general.

  * •

$\tau\doteq\\{{x}\text{:}{b}\mid{e^{\prime}}\\}$.

    1. (1)

Let $e_{\mathsf{pf}}=()$.

    2. (2)

Let $e_{p}=\texttt{bEq}_{b}\ e\ e\ e_{\mathsf{pf}}$.

    3. (3)

Let $\tau_{l}=\tau_{r}=\\{{x}\text{:}{b}\mid{x==_{b}e}\\}$.

    4. (4)

We have ${\Gamma}\vdash{x==_{b}e}\ \preceq\ {\tau}$ by SBase and semantic
typing.

    5. (5)

We find $\Gamma\vdash e_{p}\mathrel{\text{::}}\texttt{PEq}_{b}\ \\{e\\}\
\\{e\\}$ by TEqBase, with $e_{l}=e_{r}=e$. We must show:

      1. (a)

$\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{l}$ and $\Gamma\vdash
e_{r}\mathrel{\text{::}}\tau_{r}$, i.e., $\Gamma\vdash
e\mathrel{\text{::}}\\{{x}\text{:}{b}\mid{x==_{b}e}\\}$;

      2. (b)

${\Gamma}\vdash{\tau_{r}}\ \preceq\ {\\{{x}\text{:}{b}\mid{\texttt{true}}\\}}$
and ${\Gamma}\vdash{\tau_{l}}\ \preceq\
{\\{{x}\text{:}{b}\mid{\texttt{true}}\\}}$; and

      3. (c)

$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
e_{\mathsf{pf}}\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$.

    6. (6)

We find (5a) by TSelf.

    7. (7)

We find (5b) immediately by SBase.

    8. (8)

We find (5c) by TVar, using TSub to see that if
$l,r:\\{{x}\text{:}{b}\mid{x==_{b}e}\\}$ then unit will be typeable at the
refinement where both $l$ and $r$ are equal to $e$.

  * •

$\tau\doteq{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}$.

    1. (1)

$\Gamma,x:\tau_{x}\vdash e\ x\mathrel{\text{::}}\tau[x/x]$ by TApp and TVar,
noting that $\tau[x/x]=\tau$.

    2. (2)

By the IH on $\Gamma,x:\tau_{x}\vdash e\
x\mathrel{\text{::}}\tau^{\prime}[x/x]=\tau^{\prime}$, there exist
$e_{p}^{\prime},e_{\mathsf{pf}}^{\prime},\tau_{l}^{\prime},$ and
$\tau_{r}^{\prime}$ such that:

      1. (a)

${x:\tau_{x}}\vdash{\tau_{l}^{\prime}}\ \preceq\ {\tau}$ and
${x:\tau_{x}}\vdash{\tau_{r}^{\prime}}\ \preceq\ {\tau}$;

      2. (b)

$\Gamma,x:\tau_{x},l:\tau_{l}^{\prime},r:\tau_{r}^{\prime}\vdash
e_{\mathsf{pf}}^{\prime}\mathrel{\text{::}}\mathsf{pf}(e\ x,e\
x,\tau^{\prime})$; and

      3. (c)

$\Gamma,x:\tau_{x}\vdash
e_{p}^{\prime}\mathrel{\text{::}}\texttt{PEq}_{\tau^{\prime}}\ \\{e\ x\\}\
\\{e\ x\\}$.

    3. (3)

If $\tau^{\prime}=\\{{x}\text{:}{\texttt{()}}\mid{\tau^{\prime}}\\}{e\ x}{e\
x}$, then $\mathsf{pf}(e\
x,ex,b)=\\{{x}\text{:}{\texttt{()}}\mid{ex==_{b}ex}\\}$; otherwise,
$\mathsf{pf}(l,r,{x}\text{:}{\tau_{x}}\rightarrow\tau)={x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\
\\{e\ x\\}\ \\{e\ x\\}$.

In the former case, let $e_{\mathsf{pf}}^{\prime\prime}=\texttt{bEq}_{b}\ (e\
x)(e\ x)e_{\mathsf{pf}}^{\prime}$. In the latter case, let
$e_{\mathsf{pf}}^{\prime\prime}=e_{\mathsf{pf}}^{\prime}$.

Either way, we have
$\Gamma,x:\tau_{x},l:\tau_{l}^{\prime},r:\tau_{r}^{\prime}\vdash
e_{\mathsf{pf}}^{\prime\prime}\mathrel{\text{::}}\texttt{PEq}_{\tau^{\prime}}\
\\{e\ x\\}\ \\{e\ x\\}$ by TEqBase or TEqFun, respectively.

    4. (4)

Let $e_{\mathsf{pf}}={x}\text{:}{\tau_{x}}\rightarrow
e_{\mathsf{pf}}^{\prime\prime}$.

    5. (5)

Let $e_{p}=\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e\ e\
e_{\mathsf{pf}}$.

    6. (6)

Let $e_{l}=e_{r}=e$ and
$\tau_{l}={x}\text{:}{\tau_{x}}\rightarrow\tau_{l}^{\prime}$ and
$\tau_{r}={x}\text{:}{\tau_{x}}\rightarrow\tau_{r}^{\prime}$.

    7. (7)

We find subtyping by SFun and (2a).

    8. (8)

By TEqFun. We must show:

      1. (a)

$\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{l}$ and $\Gamma\vdash
e_{r}\mathrel{\text{::}}\tau_{r}$;

      2. (b)

${\Gamma}\vdash{\tau_{l}}\ \preceq\ {{x}\text{:}{\tau_{x}}\rightarrow\tau}$
and ${\Gamma}\vdash{\tau_{r}}\ \preceq\
{{x}\text{:}{\tau_{x}}\rightarrow\tau}$;

      3. (c)

$\Gamma,r:\tau_{r},l:\tau_{l}\vdash
e_{\mathsf{pf}}\mathrel{\text{::}}({x}\text{:}{\tau_{x}}\rightarrow\texttt{PEq}_{\tau}\
\\{l\ x\\}\ \\{r\ x\\})$

      4. (d)

$\Gamma\vdash{x}\text{:}{\tau_{x}}\rightarrow\tau$

    9. (9)

We find (8a) by assumption, TSub, and (7).

    10. (10)

We find (8b) by (7).

    11. (11)

We find (8c) by TLam and (2b).

  * •

$\tau\doteq\texttt{PEq}_{\tau^{\prime}}\ \\{e_{1}\\}\ \\{e_{2}\\}$. These
types are not equable, so we ignore them.

Symmetry: By induction on $\tau$.

  * •

$\tau\doteq\\{{x}\text{:}{b}\mid{e}\\}$.

    1. (1)

We have $\Gamma\vdash v_{12}\mathrel{\text{::}}\texttt{PEq}_{b}\ \\{e_{1}\\}\
\\{e_{2}\\}$.

    2. (2)

By canonical forms, $v_{12}=\texttt{bEq}_{b}\ e_{l}\ e_{r}\ v_{p}$ such that
$\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{l}$ and $\Gamma\vdash
e_{r}\mathrel{\text{::}}\tau_{r}$ (for some $\tau_{l}$ and $\tau_{r}$ that are
refinements of $b$) and $\Gamma,r:\tau_{r},l:\tau_{l}\vdash
v_{p}\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$ (Lemma
B.12).

    3. (3)

Let $v_{21}=\texttt{bEq}_{b}\ e_{r}\ e_{l}\ v_{p}$.

    4. (4)

By TEqBase, swapping $\tau_{l}$ and $\tau_{r}$ from (2). We already have
appropriate typing and subtyping derivations; we only need to see
$\Gamma,l:\tau_{l},r:\tau_{r}\vdash
v_{p}\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{r==_{b}l}\\}$.

    5. (5)

We have
${\Gamma,l:\tau_{l},r:\tau_{r}}\vdash{\\{{x}\text{:}{\texttt{()}}\mid{r==_{b}l}\\}}\
\preceq\ {\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}}$ by SBase and symmetry
of $(==_{b})$.

  * •

$\tau\doteq{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}$.

    1. (1)

We have $\Gamma\vdash
v_{12}\mathrel{\text{::}}\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}}\
\\{e_{1}\\}\ \\{e_{2}\\}$.

    2. (2)

By canonical forms,
$v_{12}=\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime\prime}}\
e_{l}\ e_{r}\ v_{p}$ such that ${\tau_{x}}\vdash{\tau_{x}^{\prime}}\ \preceq\
{a}$nd ${\tau^{\prime\prime}}\vdash{\tau^{\prime}}\ \preceq\ {a}$nd
$\Gamma\vdash e_{l}\mathrel{\text{::}}\tau_{l}$ and $\Gamma\vdash
e_{r}\mathrel{\text{::}}\tau_{r}$ (for some $\tau_{l}$ and $\tau_{r}$ that are
subtypes of ${x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime\prime}$)
and $\Gamma,r:\tau_{r},l:\tau_{l}\vdash
v_{p}\mathrel{\text{::}}{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\texttt{PEq}_{\tau^{\prime\prime}}\
\\{l\ x\\}\ \\{r\ x\\}$.

    3. (3)

By canonical forms, this time on $v_{p}$ from (2),
$v_{p}=\textsc{TLam}{x}{\tau_{x}^{\prime}}{e_{p}}$ such that
${\Gamma}\vdash{\tau_{x}}\ \preceq\ {\tau_{x}^{\prime}}$ and
$\Gamma,r:\tau_{r},l:\tau_{l},x:\tau_{x}^{\prime}\vdash
e\mathrel{\text{::}}\tau^{\prime\prime\prime}$ such that
${\Gamma,r:\tau_{r},l:\tau_{l},x:\tau_{x}^{\prime}}\vdash{\tau^{\prime\prime\prime}}\
\preceq\ {\texttt{PEq}_{\tau^{\prime\prime}}\ \\{l\ x\\}\ \\{r\ x\\}}$.

    4. (4)

By TSub, (3), and the IH on $\texttt{PEq}_{\tau^{\prime\prime}}\ \\{l\ x\\}\
\\{r\ x\\}$, we know there exists some $e_{p}^{\prime}$ such that
$\Gamma,l:\tau_{l},r:\tau_{r},x:\tau_{x}^{\prime}\vdash
e_{p}^{\prime}\mathrel{\text{::}}\texttt{PEq}_{\tau^{\prime\prime}}\ \\{r\
x\\}\ \\{l\ x\\}$.

    5. (5)

Let $v_{p}^{\prime}={x}\text{:}{\tau_{x}^{\prime}}\rightarrow e_{p}^{\prime}$.

    6. (6)

By (4) and TLam, and TSub (using subtyping from (3) and (2)),
$\Gamma,l:\tau_{l},r:\tau_{r}\vdash
v_{p}^{\prime}\mathrel{\text{::}}\texttt{PEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}}\
\\{e_{r}\ x\\}\ \\{e_{l}\ x\\}$.

    7. (7)

Let $v_{21}=\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}}\
e_{r}\ e_{l}\ v_{p}^{\prime}$.

    8. (8)

By TEqBase, with (6) for the proof and (3) and (2) for the rest.

  * •

$\tau\doteq\texttt{PEq}_{\tau^{\prime}}\ \\{e_{1}\\}\ \\{e_{2}\\}$. These
types are not equable, so we ignore them.

Transitivity: By induction on $\tau$.

  * •

$\tau\doteq\\{{x}\text{:}{b}\mid{e}\\}$.

    1. (1)

We have $\Gamma\vdash v_{12}\mathrel{\text{::}}\texttt{PEq}_{\tau}\
\\{e_{1}\\}\ \\{e_{2}\\}$ and $\Gamma\vdash
v_{23}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{2}\\}\ \\{e_{3}\\}$.

    2. (2)

By canonical forms, $v_{12}=\texttt{bEq}_{b}\ e_{1}\ e_{2}\ v_{12}^{\prime}$
such that $\Gamma\vdash e_{1}\mathrel{\text{::}}\tau_{1}$ and $\Gamma\vdash
e_{2}\mathrel{\text{::}}\tau_{2}$ (for some $\tau_{1}$ and $\tau_{2}$ that are
refinements of $b$) and $\Gamma,r:\tau_{2},l:\tau_{1}\vdash
v_{12}^{\prime}\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$.
and, similarly, $v_{23}=\texttt{bEq}_{b}\ e_{1}\ e_{2}\ v_{23}^{\prime}$ such
that $\Gamma\vdash e_{2}\mathrel{\text{::}}\tau_{2}^{\prime}$ and
$\Gamma\vdash e_{3}\mathrel{\text{::}}\tau_{3}$ (for some $\tau_{2}^{\prime}$
and $\tau_{3}$ that are refinements of $b$) and
$\Gamma,r:\tau_{3},l:\tau_{2}^{\prime}\vdash
v_{23}^{\prime}\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$.

    3. (3)

By canonical forms again, we know that
$v_{12}^{\prime}=v_{23}^{\prime}=\texttt{unit}$ and we have:

$\begin{array}[]{l}{\Gamma,r:\tau_{2},l:\tau_{1}}\vdash{\\{{x}\text{:}{\texttt{()}}\mid{x==_{\texttt{()}}\texttt{unit}}\\}}\
\preceq\
{\\{{x}\text{:}{b}\mid{\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}}\\}}\text{,
and}\\\
{\Gamma,r:\tau_{3},l:\tau_{2}^{\prime}}\vdash{\\{{x}\text{:}{\texttt{()}}\mid{x==_{\texttt{()}}\texttt{unit}}\\}}\
\preceq\
{\\{{x}\text{:}{b}\mid{\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}}\\}}.\\\
\end{array}$

    4. (4)

Elaborating on (3), we know that
$\forall\theta\in\left[\\!\left|\Gamma,r:\tau_{2},l:\tau_{1}\right|\\!\right]$,
we have:

$\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{\texttt{()}}\mid{x==_{\texttt{()}}\texttt{unit}}\\}}\right|\\!\right]\subseteq\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}}\right|\\!\right]$

and
$\forall\theta\in\left[\\!\left|\Gamma,r:\tau_{3},l:\tau_{2}^{\prime}\right|\\!\right]$,
we have:

$\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{\texttt{()}}\mid{x==_{\texttt{()}}\texttt{unit}}\\}}\right|\\!\right]\subseteq\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}}\right|\\!\right].$

    5. (5)

Since ${\\{{x}\text{:}{\texttt{()}}\mid{x==_{\texttt{()}}\texttt{unit}}\\}}$
contains all computations that terminate with unit in all models (Theorem
B.1), the right-hand sides of the equations must also hold all unit
computations. That is, all choices for $l$ and $r_{2}$ (resp. $l$ and $r$)
that are semantically well typed are necessarily equal.

    6. (6)

By (5), we can infer that in any given model, $\tau_{1}$, $\tau_{2}$,
$\tau_{2}^{\prime}$, and $\tau_{3}$ identify just one $b$-constant. Why must
$\tau_{2}$ and $\tau_{2}^{\prime}$ agree? In particular, $e_{2}$ has _both_ of
those types, but by semantic soundness (Theorem B.2), we know that it will go
to a value in the appropriate type interpretation. By determinism of
evaluation, we know it must be the _same_ value. We can therefore conclude
that
$\forall\theta\in\left[\\!\left|\Gamma,r:\tau_{3},l:\tau_{1}\right|\\!\right]$,
$\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{\texttt{()}}\mid{x==_{\texttt{()}}\texttt{unit}}\\}}\right|\\!\right]\subseteq\left[\\!\left|{\theta}\cdot{\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}}\right|\\!\right]$.

    7. (7)

By TEqBase, using $\tau_{1}$ and $\tau_{3}$ and unit as the proof. We need to
show
$\Gamma,r:\tau_{3},l:\tau_{1}\vdash\texttt{unit}\mathrel{\text{::}}\\{{x}\text{:}{\texttt{()}}\mid{l==_{b}r}\\}$;
all other premises follow from (2).

    8. (8)

By TSub and SBase, using (6) for the subtyping.

  * •

$\tau\doteq{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}$.

    1. (1)

We have $\Gamma\vdash v_{12}\mathrel{\text{::}}\texttt{PEq}_{\tau}\
\\{e_{1}\\}\ \\{e_{2}\\}$ and $\Gamma\vdash
v_{23}\mathrel{\text{::}}\texttt{PEq}_{\tau}\ \\{e_{2}\\}\ \\{e_{3}\\}$.

    2. (2)

By canonical forms, we have

$\begin{array}[]{rcl}v_{12}&=&\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}}\
e_{1}\ e_{2}\ v_{12}^{\prime}\\\
v_{23}&=&\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}}\ e_{2}\
e_{3}\ v_{23}^{\prime}\\\ \end{array}$

where there exist types $\tau_{1}$, $\tau_{2}$, $\tau_{2}^{\prime}$, and
$\tau_{3}$ subtypes of ${x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}$ such
that

$\begin{array}[]{lr}\Gamma\vdash e_{1}\mathrel{\text{::}}\tau_{1}&\Gamma\vdash
e_{2}\mathrel{\text{::}}\tau_{2}\\\ \Gamma\vdash
e_{2}\mathrel{\text{::}}\tau_{2}^{\prime}&\Gamma\vdash
e_{3}\mathrel{\text{::}}\tau_{3}\\\ \end{array}$

and there exist types $\tau_{x_{12}}$, $\tau_{x_{23}}$, $\tau^{\prime}_{12}$,
and $\tau^{\prime}_{23}$ such that

$\begin{array}[]{l}\Gamma,r:\tau_{2},l:\tau_{1}\vdash
v_{p_{12}}\mathrel{\text{::}}{x}\text{:}{\tau_{x_{12}}}\rightarrow\texttt{PEq}_{\tau^{\prime}_{12}}\
\\{l\ x\\}\ \\{r\ x\\},\\\ {\Gamma,r:\tau_{2},l:\tau_{1}}\vdash{\tau_{x}}\
\preceq\ {\tau_{x_{12}}},\\\
{\Gamma,r:\tau_{2},l:\tau_{1},x:\tau_{x}}\vdash{\tau^{\prime}_{12}}\ \preceq\
{\tau^{\prime}},\\\ \Gamma,r:\tau_{3},l:\tau_{2}^{\prime}\vdash
v_{p_{23}}\mathrel{\text{::}}{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\texttt{PEq}_{\tau^{\prime}_{23}}\
\\{l\ x\\}\ \\{r\ x\\},\\\
{\Gamma,r:\tau_{3},l:\tau_{2}^{\prime}}\vdash{\tau_{x}}\ \preceq\
{\tau_{x_{23}}},\text{ and}\\\
{\Gamma,r:\tau_{3},l:\tau_{2}^{\prime},x:\tau_{x}}\vdash{\tau^{\prime}_{23}}\
\preceq\ {\tau^{\prime}}.\end{array}$

    3. (3)

By canonical forms on $v_{p_{12}}$ and $v_{p_{23}}$ from (2), we know that:

$v_{p_{12}}=\lambda x\mathord{:}\tau_{x_{12}}.~{}e_{12}^{\prime}\qquad
v_{p_{23}}=\lambda x\mathord{:}\tau_{x_{23}}.~{}e_{23}^{\prime}$

such that:

$\begin{array}[]{l}\Gamma,r:\tau_{2},l:\tau_{1},x:\tau_{x_{12}}\vdash
e_{12}^{\prime}\mathrel{\text{::}}\tau_{12}^{\prime\prime},\\\
{\Gamma,r:\tau_{2},l:\tau_{1},x:\tau_{x_{12}}}\vdash{\tau_{12}^{\prime\prime}}\
\preceq\ {\tau^{\prime}_{12}},\\\ \\\
\Gamma,r:\tau_{3},l:\tau_{2}^{\prime},x:\tau_{x_{23}}\vdash
e_{23}^{\prime}\mathrel{\text{::}}\tau_{23}^{\prime\prime},\\\
{\Gamma,r:\tau_{3},l:\tau_{2}^{\prime},x:\tau_{x_{23}}}\vdash{\tau_{23}^{\prime\prime}}\
\preceq\ {\tau^{\prime}_{23}},\text{ and}\\\ \end{array}$

    4. (4)

By strengthening (Lemma B.7) using (2), we can replace $x$’s type with
$\tau_{x}$ in both proofs, to find:

$\begin{array}[]{l}\Gamma,r:\tau_{2},l:\tau_{1},x:\tau_{x}\vdash
e_{12}^{\prime}\mathrel{\text{::}}\tau_{12}^{\prime},\text{and}\\\
\Gamma,r:\tau_{3},l:\tau_{2}^{\prime},x:\tau_{x}\vdash
e_{23}^{\prime}\mathrel{\text{::}}\tau_{23}^{\prime}.\\\ \end{array}$

Then, by TSub, we can relax the type of the proof bodies:

$\begin{array}[]{l}\Gamma,r:\tau_{2},l:\tau_{1},x:\tau_{x}\vdash
e_{12}^{\prime}\mathrel{\text{::}}\tau^{\prime},\text{and}\\\
\Gamma,r:\tau_{3},l:\tau_{2}^{\prime},x:\tau_{x}\vdash
e_{23}^{\prime}\mathrel{\text{::}}\tau^{\prime}.\\\ \end{array}$

    5. (5)

By (4, (3), and the IH on $\texttt{PEq}_{\tau^{\prime}}\ \\{l\ x\\}\ \\{r\
x\\}$, we know there exists some proof body $e_{13}^{\prime}$ such that
$\Gamma,r:\tau_{3},l:\tau_{1}\vdash
e_{13}^{\prime}\mathrel{\text{::}}\texttt{PEq}_{\tau^{\prime}}\ \\{l\ x\\}\
\\{r\ x\\}$.

    6. (6)

Let $v_{p}={x}\text{:}{\tau_{x}}\rightarrow e_{13}^{\prime}$.

    7. (7)

By (5), and TLam.

    8. (8)

Let $v_{13}=\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}}\
e_{1}\ e_{3}\ v_{p}$.

    9. (9)

By TEqBase, with (7) for the proof and (2) for the rest.

  * •

$\tau\doteq\texttt{PEq}_{\tau^{\prime}}\ \\{e_{1}\\}\ \\{e_{2}\\}$. These
types are not equable, so we ignore them. ∎

##  Appendix C Parallel reduction and cotermination

The conventional application rule for dependent types substitutes a term into
a type, finding $e_{1}~{}e_{2}:\tau[e_{2}/x]$ when
$e_{1}:{x}\text{:}{\tau_{x}}\rightarrow\tau$. We define two logical relations:
a unary interpretation of types (Figure 8) and a binary logical relation
characterizing equivalence (Figure 10). Both of these logical relations are
defined as fixpoints on types. The type index poses a problem: the function
case of these logical relations quantify over values in the relation, but we
sometimes need to reason about expressions, not values. If
$e\hookrightarrow^{*}v$, are $\tau[e/x]$ and $\tau[v/x]$ treated the same by
our logical relations? We encounter this problem in particular in proof of
logical relation compositionality, which is precisely about exchanging
expressions in types with the values the expressions reduce to in closing
substitutions: for the unary logical relation and binary logical relation
(Lemma B.21).

The key technical device to prove these compositionality lemmas is _parallel
reduction_ (Figure 13). Parallel reduction generalizes our call-by-value
relation to allow multiple steps at once, throughout a term—even under a
lambda. Parallel reduction is a bisimulation (Lemma C.5 for forward
simulation; Corollary C.15 for backward simulation). That is, expressions that
parallel reduce to each other go to identical constants or expressions that
themselves parallel reduce, and the logical relations put terms that parallel
reduce in the same equivalence class.

To prove the compositionality lemmas, we first show that (a) the logical
relations are closed under parallel reduction ( for the unary relation and
Lemma B.20 for the binary relation) and (b) use the backward simulation to
change values in the closing substitution to a substituted expression in the
type.

Our proof comes in three steps. First, we establish some basic properties of
parallel reduction (§C.1). Next, proving the forward simulation is
straightforward (§C.2): if $e_{1}\rightrightarrows e_{2}$ and
$e_{1}\hookrightarrow e_{1}^{\prime}$, then either parallel reduction
contracted the redex for us and $e_{1}^{\prime}\rightrightarrows e_{2}$
immediately, or the redex is preserved and $e_{2}\hookrightarrow
e_{2}^{\prime}$ such that $e_{1}^{\prime}\rightrightarrows e_{2}^{\prime}$.
Proving the backward simulation is more challenging (§C.3). If
$e_{1}\rightrightarrows e_{2}$ and $e_{2}\hookrightarrow e_{2}^{\prime}$, the
redex contracted in $e_{2}$ may not yet be exposed. The trick is to show a
tighter bisimulation, where the outermost constructors are always the same,
with the subparts parallel reducing. We call this relation _congruence_
(Figure 14); it’s a straightforward restriction of parallel reduction,
eliminating $\beta$, eq1, and eq2 as outermost constructors (but allowing them
deeper inside). The key lemma shows that if $e_{1}\rightrightarrows e_{2}$,
then there exists $e_{1}^{\prime}$ $e_{1}\hookrightarrow^{*}e_{1}^{\prime}$
such that $e_{1}^{\prime}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}$ (Lemma C.11). Once we know that parallel reduction implies
reduction to congruent terms, proving that congruence is a backward simulation
allows us to reason “up to congruence”. In particular, congruence is a sub-
relation of parallel reduction, so we find that parallel reduction is a
backward simulation. Finally, we can show that $e_{1}\rightrightarrows e_{2}$
implies observational equivalence (§C.4); for our purposes, it suffices to
find cotermination at constants (Corollary C.17).

One might think, in light of Takahashi’s explanation of parallel reduction
(Takahashi, 1989), that the simulation techniques we use are too powerful for
our needs: why not simply rely on the Church-Rosser property and confluence,
which she proves quite simply? Her approach works well when relating parallel
reduction to full $\beta$-reduction (and/or $\eta$-reduction): the transitive
closure of her parallel reduction relation is equal to the transitive closure
of plain $\beta$-reduction (resp. $\eta$\- and $\beta\eta$-reduction). But
we’re interested in programming languages, so our underlying reduction
relation isn’t full $\beta$: we use call-by-value, and we will never reduce
under lambdas. But even if we were call-by-name, we would have the same issue.
Parallel reduction implies reduction, but not to the _same_ value, as in her
setting. Parallel reduction yields values that are equivalent, _up to parallel
reduction and congruence_ (see, e.g., Corollary C.13).

$e\rightrightarrows e$

$\inference{}{x\rightrightarrows x}[var]\quad\inference{}{c\rightrightarrows
c}[const]\quad\inference{\tau\rightrightarrows\tau^{\prime}\quad
e\rightrightarrows e^{\prime}}{\lambda
x\mathord{:}\tau.~{}e\rightrightarrows\lambda
x\mathord{:}\tau^{\prime}.~{}e^{\prime}}[lam]\quad\inference{e_{1}\rightrightarrows
e_{1}^{\prime}\quad e_{2}\rightrightarrows e_{2}^{\prime}}{e_{1}\
e_{2}\rightrightarrows e_{1}^{\prime}\ e_{2}^{\prime}}[app]$

$\inference{e\rightrightarrows e^{\prime}\quad v\rightrightarrows
v^{\prime}}{(\lambda x\mathord{:}\tau.~{}e)\ v\rightrightarrows
e^{\prime}[v^{\prime}/x]}[\beta]\quad\inference{}{(==_{b})\
c_{1}\rightrightarrows(==_{(c_{1},b)})}[eq1]\quad\inference{}{(==_{(c_{1},b)})\
c_{2}\rightrightarrows c_{1}=c_{2}}[eq2]$

$\inference{e_{l}\rightrightarrows e_{l}^{\prime}\quad e_{r}\rightrightarrows
e_{r}^{\prime}\quad e\rightrightarrows e^{\prime}}{\texttt{bEq}_{b}\ e_{l}\
e_{r}\ e\rightrightarrows\texttt{bEq}_{b}\ e_{l}^{\prime}\ e_{r}^{\prime}\
e^{\prime}}[beq]\quad\inference{\tau_{x}\rightrightarrows\tau_{x}^{\prime}\quad\tau\rightrightarrows\tau^{\prime}\quad
e_{l}\rightrightarrows e_{l}^{\prime}\quad e_{r}\rightrightarrows
e_{r}^{\prime}\quad e\rightrightarrows
e^{\prime}}{\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\
e\rightrightarrows\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime}}\
e_{l}^{\prime}\ e_{r}^{\prime}\ e^{\prime}}[xeq]$

$\tau\rightrightarrows\tau$

$\inference{r\rightrightarrows
r^{\prime}}{\\{{x}\text{:}{b}\mid{r}\\}\rightrightarrows\\{{x}\text{:}{b}\mid{r^{\prime}}\\}}[ref]\quad\inference{\tau_{x}\rightrightarrows\tau_{x}^{\prime}\quad\tau\rightrightarrows\tau^{\prime}}{{x}\text{:}{\tau_{x}}\rightarrow\tau\rightrightarrows{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime}}[fun]$

$\inference{\tau\rightrightarrows\tau^{\prime}\quad e_{l}\rightrightarrows
e_{l}^{\prime}\quad e_{r}\rightrightarrows
e_{r}^{\prime}}{\texttt{PEq}_{\tau}\ \\{e_{l}\\}\
\\{e_{r}\\}\rightrightarrows\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}^{\prime}\\}\ \\{e_{r}^{\prime}\\}}[eq]$

Figure 13. Parallel reduction in terms and types.

###  C.1. Basic Properties

###### Lemma C.1 (Parallel reduction is reflexive).

For all $e$ and $\tau$, $e\rightrightarrows e$ and
$\tau\rightrightarrows\tau$.

###### Proof.

By mutual induction on $e$ and $\tau$.

##### Expressions

  * •

$e\doteq x$. By var.

  * •

$e\doteq c$. By const.

  * •

$e\doteq\lambda x\mathord{:}\tau.~{}e^{\prime}$. By the IHs on $\tau$ and
$e^{\prime}$ and lam.

  * •

$e\doteq e_{1}~{}e_{2}$. By the IH on $e_{1}$ and $e_{2}$ and app.

  * •

$e\doteq\texttt{bEq}_{b}\ e_{l}\ e_{r}\ e^{\prime}$. By the IHs on $e_{l}$,
$e_{r}$, and $e^{\prime}$ and beq.

  * •

$e\doteq\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\
e^{\prime}$. By the IHs on $\tau_{x}$, $\tau$, $e_{l}$, $e_{r}$, and
$e^{\prime}$ and xeq.

##### Types

  * •

$\tau\doteq\\{{x}\text{:}{b}\mid{r}\\}$. By the IH on $r$ (an expression) and
ref.

  * •

$\tau\doteq{x}\text{:}{\tau_{x}}\rightarrow\tau^{\prime}$. By the IHs on
$\tau_{x}$ and $\tau^{\prime}$ and fun.

  * •

$\tau\doteq\texttt{PEq}_{\tau^{\prime}}\ \\{e_{l}\\}\ \\{e_{r}\\}$. By the IHs
on $\tau^{\prime}$, $e_{l}$, and $e_{r}$ and eq. ∎

###### Lemma C.2 (Parallel reduction is substitutive).

If $e\rightrightarrows e^{\prime}$, then:

  1. (1)

If $e_{1}\rightrightarrows e_{2}$, then $e_{1}[e/x]\rightrightarrows
e_{2}[e^{\prime}/x]$.

  2. (2)

If $\tau_{1}\rightrightarrows\tau_{2}$, then
$\tau_{1}[e/x]\rightrightarrows\tau_{2}[e^{\prime}/x]$.

###### Proof.

By mutual induction on $e_{1}$ and $\tau_{1}$.

##### Expressions

  * var

$y\rightrightarrows y$. If $y\neq x$, then the substitution has no effect and
the case is trivial. If $y=x$, then $x[e/x]=e$ and we have $e\rightrightarrows
e^{\prime}$ by assumption. We have $e\rightrightarrows e$ by reflexivity
(Lemma C.1).

  * const

$c\rightrightarrows c$. This case is trivial: the substitution has no effect.

  * lam

$\lambda y\mathord{:}\tau.~{}e^{\prime}\rightrightarrows\lambda
y\mathord{:}\tau.~{}e^{\prime\prime}$. If $y\neq x$, then by the IH on
$e^{\prime}$ and lam. If $y=x$, then the substitution has no effect and the
case is trivial.

  * app

$e_{11}\ e_{12}\rightrightarrows e_{21}\ e_{22}$, where
$e{1i}\rightrightarrows e{2i}$ for $i=1,2$. By the IHs on $e_{1i}$ and app.

  * beta

$(\lambda y\mathord{:}\tau.~{}e^{\prime})\ v\rightrightarrows
e^{\prime}[v^{\prime}/y]$, where $e^{\prime}\rightrightarrows
e^{\prime\prime}$ and $v\rightrightarrows v^{\prime}$. If $y\neq x$, then
$(\lambda y\mathord{:}\tau.~{}e^{\prime}[e/x])\ v[e/x]\rightrightarrows
e^{\prime\prime}[e/x][v^{\prime}[e/x]/y]$ by $\beta$. Since $y\neq x$,
$e^{\prime\prime}[e/x][v^{\prime}[e/x]/y]=e^{\prime\prime}[v^{\prime}/y][e/x]$
as desired.

If $y=x$, then the substitution in the lambda has no effect, and we find
$(\lambda x\mathord{:}\tau.~{}e^{\prime})\ v[e/x]\rightrightarrows
e^{\prime\prime}[v^{\prime}[e/x]/x]$ by $\beta$. We have
$e^{\prime\prime}[v^{\prime}[e/x]/x]=e^{\prime\prime}[v^{\prime}/x][e/x]$ as
desired.

  * eq1

$(==_{b})\ c_{1}\rightrightarrows(==_{(c_{1},b)})$. This case is trivial by
eq1, as the substitution has no effect.

  * eq2

$(==_{(c_{1},b)})\ c_{2}\rightrightarrows c_{1}=c_{2}$. This case is trivial
by eq2, as the substitution has no effect.

  * beq

$\texttt{bEq}_{b}\ e_{l}\ e_{r}\ e_{p}\rightrightarrows\texttt{bEq}_{b}\
e_{l}^{\prime}\ e_{r}^{\prime}\ e_{p}^{\prime}$, where $e_{l}\rightrightarrows
e_{l}^{\prime}$ and $e_{r}\rightrightarrows e_{r}^{\prime}$ and
$e_{p}\rightrightarrows e_{p}^{\prime}$. By the IHs on $e_{l}$, $e_{r}$, and
$e_{p}$ and beq.

  * xeq

$\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\
e_{p}\rightrightarrows\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
e_{l}^{\prime}\ e_{r}^{\prime}\ e_{p}^{\prime}$, where $e_{l}\rightrightarrows
e_{l}^{\prime}$ and $e_{r}\rightrightarrows e_{r}^{\prime}$ and
$e_{p}\rightrightarrows e_{p}^{\prime}$. By the IHs on $e_{l}$, $e_{r}$, and
$e_{p}$ and xeq.

##### Types

  * ref

$\\{{y}\text{:}{b}\mid{r}\\}\rightrightarrows\\{{y}\text{:}{b}\mid{r^{\prime}}\\}$
where $r\rightrightarrows r^{\prime}$. If $y\neq x$, then
$r[e/x]\rightrightarrows r^{\prime}[e^{\prime}/x]$ by the IH on $r$; we are
done by ref.

If $y=x$, then the substitution has no effect, and the case is immediate by
reflexivity (Lemma C.1).

  * fun

${y}\text{:}{\tau_{y}}\rightarrow\tau\rightrightarrows{y}\text{:}{\tau_{y}^{\prime}}\rightarrow\tau^{\prime}$
where $\tau_{y}\rightrightarrows\tau_{y}^{\prime}$ and
$\tau\rightrightarrows\tau^{\prime}$. If $y\neq x$, then by the IH on
$\tau_{y}$ and $\tau$ and fun.

If $y=x$, then the substitution only has effect in the domain. The IH on
$\tau_{y}$ finds
$\tau_{y}[e/x]\rightrightarrows\tau_{y}^{\prime}[e^{\prime}/x]$ in the domain;
reflexivity covers the codomain (Lemma C.1), and we are done by fun.

  * eq

$\texttt{PEq}_{\tau}\ \\{e_{l}\\}\
\\{e_{r}\\}\rightrightarrows\texttt{PEq}_{\tau^{\prime}}\
\\{e_{l}^{\prime}\\}\ \\{e_{r}^{\prime}\\}$. By the IHs and eq. ∎

###### Corollary C.3 (Substituting multiple parallel reduction is parallel
reduction).

If $e_{1}\rightrightarrows^{*}e_{2}$, then
$e[e_{1}/x]\rightrightarrows^{*}e[e{2}/x]$.

###### Proof.

First, notice that $e\rightrightarrows e$ by reflexivity (Lemma C.1). By
induction on $e_{1}\rightrightarrows^{*}e_{2}$, using reflexivity in the base
case (Lemma C.1); the inductive step uses substituting parallel reduction
(Lemma C.2) and the IH. ∎

###### Lemma C.4 (Parallel reduction subsumes reduction).

If $e_{1}\hookrightarrow e_{2}$ then $e_{1}\rightrightarrows e_{2}$.

###### Proof.

By induction on the evaluation derivation, using reflexivity of parallel
reduction to cover expressions and types that didn’t step (Lemma C.1).

  * ctx

$\mathcal{E}[e]\hookrightarrow\mathcal{E}[e^{\prime}]$, where
$e\hookrightarrow e^{\prime}$. By the IH, $e\rightrightarrows e^{\prime}$. By
structural induction on $\mathcal{E}$.

    * –

$\mathcal{E}\doteq\bullet$. By the outer IH.

    * –

$\mathcal{E}\doteq\mathcal{E}_{1}\ e_{2}$. By the inner IH on
$\mathcal{E}_{1}$, reflexivity on $e_{2}$, and app.

    * –

$\mathcal{E}\doteq v_{1}\ \mathcal{E}_{2}$. By reflexivity on $v_{1}$, the
inner IH on $\mathcal{E}_{2}$, and app.

    * –

$\mathcal{E}\doteq\texttt{bEq}_{b}\ e_{l}\ e_{r}\ \mathcal{E}^{\prime}$. By
reflexivity on $e_{l}$ and $e_{r}$, the inner IH on and
$\mathcal{E}^{\prime}$, and beq.

    * –

$\mathcal{E}\doteq\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\
e_{r}\ \mathcal{E}^{\prime}$. By reflexivity on $\tau_{x}$, $\tau$, $e_{l}$
and $e_{r}$, the inner IH on and $\mathcal{E}^{\prime}$, and xeq.

  * $\beta$

$(\lambda x\mathord{:}\tau.~{}e)\ v\hookrightarrow e[v/x]$. By reflexivity
(Lemma C.1, $e\rightrightarrows e$ and $v\rightrightarrows v$. By beta,
$(\lambda x\mathord{:}\tau.~{}e)\ v\rightrightarrows e[v/x]$.

  * eq1

By eq1.

  * eq2

By eq2. ∎

###  C.2. Forward Simulation

###### Lemma C.5 (Parallel reduction is a forward simulation).

If $e_{1}\rightrightarrows e_{2}$ and $e_{1}\hookrightarrow e_{1}^{\prime}$,
then there exists $e_{2}^{\prime}$ such that
$e_{2}\hookrightarrow^{*}e_{2}^{\prime}$ and $e_{1}^{\prime}\rightrightarrows
e_{2}^{\prime}$.

###### Proof.

By induction on the derivation of $e_{1}\hookrightarrow e_{1}^{\prime}$,
leaving $e_{2}$ general.

  * ctx

By structural induction on $\mathcal{E}$, using reflexivity (Lemma C.1) on
parts where the IH doesn’t apply.

    * –

$\mathcal{E}\doteq\bullet$. By the outer IH on the actual step.

    * –

$\mathcal{E}\doteq\mathcal{E}_{1}\ e_{2}$. By the IH on $\mathcal{E}_{1}$,
reflexivity on $e_{2}$, and app.

    * –

$\mathcal{E}\doteq v_{1}\ \mathcal{E}_{2}$. By reflexivity on $v_{1}$, the IH
on $\mathcal{E}_{2}$, and app.

    * –

$\mathcal{E}\doteq\texttt{bEq}_{b}\ e_{l}\ e_{r}\ \mathcal{E}^{\prime}$. By
reflexivity on $e_{l}$ and $e_{r}$, the IH on $\mathcal{E}^{\prime}$, and beq.

    * –

$\mathcal{E}\doteq\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\
e_{r}\ \mathcal{E}^{\prime}$. By reflexivity on $\tau_{x}$, $\tau$, $e_{l}$
and $e_{r}$, the IH on $\mathcal{E}^{\prime}$, and xeq.

  * $\beta$

$(\lambda x\mathord{:}\tau.~{}e)\ v\hookrightarrow e[v/x]$. One of two rules
could have applied to find $e_{1}\rightrightarrows e_{2}$: app or $\beta$.

In the app case, we have $e_{2}=(\lambda
x\mathord{:}\tau^{\prime}.~{}e^{\prime})\ v^{\prime}$ where
$\tau\rightrightarrows\tau^{\prime}$ and $e\rightrightarrows e^{\prime}$ and
$v\rightrightarrows v^{\prime}$. Let
$e_{2}^{\prime}=e^{\prime}[v^{\prime}/x]$. We find
$e_{2}\hookrightarrow^{*}e_{2}^{\prime}$ in one step by $\beta$. We find
$e[v/x]\rightrightarrows e^{\prime}[v^{\prime}/x]$ by substitutivity of
parallel reduction (Lemma C.2).

In the $\beta$ case, we have $e_{2}=e^{\prime}[v^{\prime}/x]$ such that
$e\rightrightarrows e^{\prime}$ and $v\rightrightarrows v^{\prime}$. Let
$e_{2}^{\prime}=e_{2}$. We find $e_{2}\hookrightarrow^{*}e_{2}^{\prime}$ in no
steps at all; we find $e_{1}^{\prime}\rightrightarrows e_{2}^{\prime}$ by
substitutivity of parallel reduction (Lemma C.2).

  * eq1

$(==_{b})\ c_{1}\hookrightarrow(==_{(c_{1},b)})$. One of two rules could have
applied to find $(==_{b})\ c_{1}\rightrightarrows e_{2}$: app or eq1.

In the app case, we must have $e_{2}=e_{1}=(==_{b})\ c_{1}$, because there are
no reductions available in these constants. Let
$e_{2}^{\prime}=(==_{(c_{1},b)})$. We find
$e_{2}\hookrightarrow^{*}e_{2}^{\prime}$ in a single step by our assumption
(or eq1). We find parallel reduction by reflexivity (Lemma C.1).

In the eq2 case, we have $e_{2}=e_{1}^{\prime}=(==_{(c_{1},b)})$. Let
$e_{2}^{\prime}=e_{2}$. We find $e_{2}\hookrightarrow^{*}e_{2}^{\prime}$ in no
steps at all. We find parallel reduction by reflexivity (Lemma C.1).

  * eq2

$(==_{(c_{1},b)})\ c_{2}\hookrightarrow c_{1}=c_{2}$. One of two rules could
have applied to find $(==_{(c_{1},b)})\ c_{2}\rightrightarrows e_{2}$: app or
eq2.

In the app case, we have $e_{2}=e_{1}={(==_{(c_{1},b)})\ c_{2}}$, because
there are no reductions available in these constants. Let
$e_{2}^{\prime}\doteq c_{1}=c_{2}$, i.e. true when $c_{1}=c_{2}$ and false
otherwise. We find $e_{2}\hookrightarrow^{*}e_{2}^{\prime}$ in a single step
by our assumption (or eq2). We find parallel reduction by reflexivity (Lemma
C.1).

In the eq2 case, we have $e_{2}=e_{1}^{\prime}\doteq c_{1}=c_{2}$, i.e. true
when $c_{1}=c_{2}$ and false otherwise. Let $e_{2}^{\prime}=e_{2}$. We find
$e_{2}\hookrightarrow^{*}e_{2}^{\prime}$ in no steps at all. We find parallel
reduction by reflexivity (Lemma C.1). ∎

###  C.3. Backward Simulation

###### Lemma C.6 (Reduction is substitutive).

If $e_{1}\hookrightarrow e_{2}$, then $e_{1}[e/x]\hookrightarrow e_{2}[e/x]$.

###### Proof.

By induction on the derivation of $e_{1}\hookrightarrow e_{2}$.

  * ctx

By structural induction on $\mathcal{E}$.

    * –

$\mathcal{E}\doteq\bullet$. By the outer IH.

    * –

$\mathcal{E}\doteq\mathcal{E}_{1}\ e_{2}$. By the IH on $\mathcal{E}_{1}$ and
ctx.

    * –

$\mathcal{E}\doteq v_{1}\ \mathcal{E}_{2}$. By the IH on $\mathcal{E}_{2}$ and
ctx.

    * –

$\mathcal{E}\doteq\texttt{bEq}_{b}\ e_{l}\ e_{r}\ \mathcal{E}^{\prime}$. By
the IH on $\mathcal{E}^{\prime}$ and ctx.

    * –

$\mathcal{E}\doteq\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\
e_{r}\ \mathcal{E}^{\prime}$. By the IH on $\mathcal{E}^{\prime}$ and ctx.

  * $\beta$

$(\lambda y\mathord{:}\tau.~{}e^{\prime})\ v\hookrightarrow e^{\prime}[v/y]$.
We must show $(\lambda y\mathord{:}\tau.~{}e^{\prime})[e/x]\
v[e/x]\hookrightarrow e^{\prime}[v/y][e/x]$.

The exact result depends on whether $y=x$. If $y\neq x$, the substitution goes
through, and we have $(\lambda y\mathord{:}\tau.~{}e^{\prime})[e/x]=\lambda
y\mathord{:}\tau[e/x].~{}e^{\prime}[e/x]$. By $\beta$, $(\lambda
y\mathord{:}\tau[e/x].~{}e^{\prime}[e/x])\ v[e/x]\hookrightarrow
e^{\prime}[e/x][v[e/x]/y]$. But
$e^{\prime}[e/x][v[e/x]/y]=e^{\prime}[v/y][e/x]$, and we are done.

If, on the other hand, $y=x$, then the substitution has no effect in the body
of the lambda, and $(\lambda y\mathord{:}\tau.~{}e^{\prime})[e/x]=\lambda
y\mathord{:}\tau[e/x].~{}e^{\prime}$. By $\beta$ again, we find $(\lambda
y\mathord{:}\tau[e/x].~{}e^{\prime})\ v[e/x]\hookrightarrow
e^{\prime}[v[e/x]/y]$. Since $y=x$, we really have $e^{\prime}[v[e/x]/x]$
which is the same as $e^{\prime}[v/x][e/x]=e^{\prime}[v/y][e/x]$, as desired.

  * eq1

The substitution has no effect; immediate, by eq1.

  * eq2

The substitution has no effect; immediate, by eq2. ∎

###### Corollary C.7 (Multi-step reduction is substitutive).

If $e_{1}\hookrightarrow^{*}e_{2}$, then
$e_{1}[e/x]\hookrightarrow^{*}e_{2}[e/x]$.

###### Proof.

By induction on the derivation of $e_{1}\hookrightarrow^{*}e_{2}$. The base
case is immediate ($e_{1}=e_{2}$, and we take no steps). The inductive case
follows by the IH and single-step substitutivity (Lemma C.6). ∎

$\inference{}{x\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}x}[var]\quad\inference{}{c\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}c}[const]\quad\inference{\tau\rightrightarrows\tau^{\prime}\quad
e\rightrightarrows e^{\prime}}{\lambda
x\mathord{:}\tau.~{}e\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\lambda
x\mathord{:}\tau^{\prime}.~{}e^{\prime}}[lam]\quad\inference{e_{1}\rightrightarrows
e_{1}^{\prime}\quad e_{2}\rightrightarrows e_{2}^{\prime}}{e_{1}\
e_{2}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{1}^{\prime}\ e_{2}^{\prime}}[app]$

$\inference{e_{l}\rightrightarrows e_{l}^{\prime}\quad e_{r}\rightrightarrows
e_{r}^{\prime}\quad e\rightrightarrows e^{\prime}}{\texttt{bEq}_{b}\ e_{l}\
e_{r}\ e\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\texttt{bEq}_{b}\ e_{l}^{\prime}\ e_{r}^{\prime}\
e^{\prime}}[beq]\quad\inference{\tau_{x}\rightrightarrows\tau_{x}^{\prime}\quad\tau\rightrightarrows\tau^{\prime}\quad
e_{l}\rightrightarrows e_{l}^{\prime}\quad e_{r}\rightrightarrows
e_{r}^{\prime}\quad e\rightrightarrows
e^{\prime}}{\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\
e\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime}}\
e_{l}^{\prime}\ e_{r}^{\prime}\ e^{\prime}}[xeq]$

Figure 14. Term congruence.

We say terms are _congruent_ when they (a) have the same outermost constructor
and (b) their subparts parallel reduce to each other.444Congruent terms are
related to Takahashi’s $\tilde{M}$ operator: in that they characterize
parallel reductions that preserve structure. They are not the same, though:
Takahashi’s $\tilde{M}$ will do $\beta\eta$-reductions on outermost redexes.
That is, $\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\subseteq\rightrightarrows$, where the outermost rule must be one of
var, const, lam, app, beq, or xeq and cannot be a _real_ reduction like
$\beta$, eq1, or eq2.

Congruence is a key tool in proving that parallel reduction is a backward
simulation. Parallel reductions under a lambda prevent us from having an “on-
the-nose” relation, but reduction can keep up enough with parallel reduction
to maintain congruence.

###### Lemma C.8 (Congruence implies parallel reduction).

If $e_{1}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}$ then $e_{1}\rightrightarrows e_{2}$.

###### Proof.

By induction on the derivation of
$e_{1}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}$.

  * var

$x\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}x$. By var.

  * const

$c\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}c$. By const.

  * lam

$\lambda x\mathord{:}\tau.~{}e\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\lambda x\mathord{:}\tau^{\prime}.~{}e^{\prime}$, with
$\tau\rightrightarrows\tau^{\prime}$ and $e\rightrightarrows e^{\prime}$. By
lam.

  * app

$e_{1}\ e_{2}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{1}^{\prime}\ e_{2}^{\prime}$, with $e_{1}\rightrightarrows
e_{1}^{\prime}$ and $e_{2}\rightrightarrows e_{2}^{\prime}$. By app.

  * beq

$\texttt{bEq}_{b}\ e_{l}\ e_{r}\ e\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\texttt{bEq}_{b}\ e_{l}^{\prime}\ e_{r}^{\prime}\ e$, with
$e_{l}\rightrightarrows e_{l}^{\prime}$ and $e_{r}\rightrightarrows
e_{r}^{\prime}$ and $e\rightrightarrows e^{\prime}$. By beq.

  * xeq

By xeq. $\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\
e\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}^{\prime}\
e_{r}^{\prime}\ e$, with $\tau_{x}\rightrightarrows\tau_{x}^{\prime}$ and
$\tau\rightrightarrows\tau^{\prime}$ and $e_{l}\rightrightarrows
e_{l}^{\prime}$ and $e_{r}\rightrightarrows e_{r}^{\prime}$ and
$e\rightrightarrows e^{\prime}$. By xeq. ∎

We need to strengthen substitutivity (Lemma C.2) to show that it preserves
congruence.

###### Corollary C.9 (Congruence is substitutive).

If $e_{1}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{1}^{\prime}$ and $e_{2}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}^{\prime}$, then
$e_{1}[e_{2}/x]\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}[e_{2}^{\prime}/x]$.

###### Proof.

By cases on $e_{1}$.

  * •

$e_{1}=y$. It must be that $e_{2}=y$ as well, since only var could have
applied. If $y\neq x$, then the substitution has no effect and we have
$y\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}y$ by assumption (or var). If $x=y$, then $e_{1}[e_{2}/x]=e_{2}$ and
we have $e_{2}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}^{\prime}$ by assumption.

  * •

$e_{1}=c$. It must be that $e_{2}=c$ as well. The substitution has no effect;
immediate by var.

  * •

$e_{1}=\lambda y\mathord{:}\tau.~{}e$. It must be that $e_{2}=\lambda
y\mathord{:}\tau^{\prime}.~{}e^{\prime}$ such that
$\tau\rightrightarrows\tau^{\prime}$ and $e\rightrightarrows e^{\prime}$. If
$y\neq x$, then we must show $\lambda
y\mathord{:}\tau[e_{2}/x].~{}e[e_{2}/x]\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\lambda
y\mathord{:}\tau^{\prime}[e_{2}^{\prime}/x].~{}e^{\prime}[e_{2}^{\prime}/x]$,
which we have immediately by lam and Lemma C.2 on our two subparts. If $y=x$,
then we must show $\lambda
y\mathord{:}\tau[e_{2}/x].~{}e\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\lambda y\mathord{:}\tau^{\prime}[e_{2}^{\prime}/x].~{}e^{\prime}$,
which we have immediately by lam, Lemma C.2 on our
$\tau\rightrightarrows\tau^{\prime}$, and the fact that $e\rightrightarrows
e^{\prime}$.

  * •

$e_{1}=e_{11}\ e_{12}$. It must be that $e_{2}=e_{21}\ e_{22}$, such that
$e_{11}\rightrightarrows e_{21}$ and $e_{12}\rightrightarrows e_{22}$. By app
and Lemma C.2 on the subparts.

  * •

$e_{1}=\texttt{bEq}_{b}\ e_{l}\ e_{r}\ e$. It must be the case that
$e_{2}=\texttt{bEq}_{b}\ e_{l}^{\prime}\ e_{r}^{\prime}\ e^{\prime}$ where
$e_{l}\rightrightarrows e_{l}^{\prime}$ and $e_{r}\rightrightarrows
e_{r}^{\prime}$. By beq and Lemma C.2 on the subparts.

  * •

$e_{1}=\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\ e$.
It must be the case that
$e_{2}=\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime}}\
e_{l}^{\prime}\ e_{r}^{\prime}\ e^{\prime}$ where $e_{l}\rightrightarrows
e_{l}^{\prime}$ (and similarly for $\tau_{x}$, $\tau$, $e_{r}$, and $e$). By
xeq and Lemma C.2 on the subparts. ∎

###### Lemma C.10 (Parallel reduction of values implies congruence).

If $v_{1}\rightrightarrows v_{2}$ then
$v_{1}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v_{2}$.

###### Proof.

By induction on the derivation of $v_{1}\rightrightarrows v_{2}$.

  * var

Contradictory: variables aren’t values.

  * const

Immediate, by const.

  * lam

Immediate, by lam.

  * app

Contradictory: applications aren’t values.

  * beq

Immediate, by beq.

  * xeq

Immediate, by xeq.

  * $\beta$

Contradictory: applications aren’t values.

  * eq1

Contradictory: applications aren’t values.

  * eq2

Contradictory: applications aren’t values. ∎

###### Lemma C.11 (Parallel reduction implies reduction to congruent forms).

If $e_{1}\rightrightarrows e_{2}$, then there exists $e_{1}^{\prime}$
$e_{1}\hookrightarrow^{*}e_{1}^{\prime}$ such that
$e_{1}^{\prime}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}$.

###### Proof.

By induction on $e_{1}\rightrightarrows e_{2}$.

##### Structural rules

  * var

$x\rightrightarrows x$. We have $e_{1}=e_{2}=x$ by var.

  * const

$c\rightrightarrows c$. We have $e_{1}=e_{2}=c$ by const.

  * lam

$\lambda x\mathord{:}\tau.~{}e\rightrightarrows\lambda
x\mathord{:}\tau^{\prime}.~{}e^{\prime}$, where
$\tau\rightrightarrows\tau^{\prime}$ and $e\rightrightarrows e^{\prime}$.
Immediate, by lam.

  * app

$e_{11}\ e_{12}\rightrightarrows e_{21}\ e_{22}$, where
$e_{11}\rightrightarrows e_{21}$ and $e_{12}\rightrightarrows e_{22}$.
Immediate, by app.

  * beq

$\texttt{bEq}_{b}\ e_{l}\ e_{r}\ e\rightrightarrows\texttt{bEq}_{b}\
e_{l}^{\prime}\ e_{r}^{\prime}\ e^{\prime}$ where $e_{l}\rightrightarrows
e_{l}^{\prime}$ and $e_{r}\rightrightarrows e_{r}^{\prime}$ and
$e\rightrightarrows e^{\prime}$. Immediate, by beq.

  * xeq

$\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\
e\rightrightarrows\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime}}\
e_{l}^{\prime}\ e_{r}^{\prime}\ e^{\prime}$ where
$\tau_{x}\rightrightarrows\tau_{x}^{\prime}$ and
$\tau\rightrightarrows\tau^{\prime}$ and $e_{l}\rightrightarrows
e_{l}^{\prime}$ and $e_{r}\rightrightarrows e_{r}^{\prime}$ and
$e\rightrightarrows e^{\prime}$. Immediate, by xeq.

##### Reduction rules

These are the more interesting cases, where the parallel reduction does a
reduction step—ordinary reduction has to do more work to catch up.

  * $\beta$

$(\lambda x\mathord{:}\tau.~{}e)\ v\rightrightarrows
e^{\prime}[v^{\prime}/x]$, where $e\rightrightarrows e^{\prime\prime}$ and
$v\rightrightarrows v^{\prime\prime}$.

We have $(\lambda x\mathord{:}\tau.~{}e)\ v\hookrightarrow e[v/x]$ by $\beta$.
By the IH on $e\rightrightarrows e^{\prime\prime}$, there exists $e^{\prime}$
such that $e\hookrightarrow^{*}e^{\prime}$ such that
$e^{\prime}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e^{\prime\prime}$. We _ignore_ the IH on $v\rightrightarrows
v^{\prime\prime}$, noticing instead that parallel reducing values are
congruent (Lemma C.10) and so $v\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v^{\prime\prime}$. Since reduction is substitutive (Corollary C.7), we
can find that $e[v/x]\hookrightarrow^{*}e^{\prime}[v/x]$. Since congruence is
substitutive (Lemma C.9), we have
$e^{\prime}[v/x]\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e^{\prime\prime}[v^{\prime\prime}/x]$, as desired.

  * eq1

$(==_{b})\ c_{1}\rightrightarrows(==_{(c_{1},b)})$. We have $(==_{b})\
c_{1}\hookrightarrow(==_{(c_{1},b)})$ in a single step; we find congruence by
const.

  * eq2

$(==_{(c_{1},b)})\ c_{2}\rightrightarrows c_{1}=c_{2}$. We have
$(==_{(c_{1},b)})\ c_{2}\hookrightarrow c_{1}=c_{2}$ in a single step; we find
congruence by const. ∎

###### Lemma C.12 (Congruence to a value implies reduction to a value).

If $e\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v^{\prime}$ then $e\hookrightarrow^{*}v$ such that
$v\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v^{\prime}$.

###### Proof.

By induction on $v^{\prime}$.

  * •

$v^{\prime}\doteq c$. It must be the case that $e=c$. Let $v=c$. By const.

  * •

$v^{\prime}\doteq\lambda x\mathord{:}\tau^{\prime}.~{}e^{\prime\prime}$. It
must be the case that $e=\lambda x\mathord{:}\tau.~{}e^{\prime}$ such that
$\tau\rightrightarrows\tau^{\prime}$ and $e\rightrightarrows
e^{\prime\prime}$. By lam.

  * •

$v\doteq\texttt{bEq}_{b}\ e_{l}^{\prime}\ e_{r}^{\prime}\ v_{p}^{\prime}$. It
must be the case that $e=\texttt{bEq}_{b}\ e_{l}\ e_{r}\ e_{p}$ where
$e_{l}\rightrightarrows e_{l}^{\prime}$ and $e_{r}\rightrightarrows
e_{r}^{\prime}$ and $e_{p}\rightrightarrows v_{p}^{\prime}$. Since parallel
reduction implies reduction to congruent forms (Lemma C.11), we have
$e_{p}\hookrightarrow^{*}e_{p}^{\prime}$ and
$e_{p}^{\prime}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v_{p}^{\prime}$. By the IH on $v_{p}^{\prime}$, we know that
$e_{p}^{\prime}\hookrightarrow^{*}v_{p}$ such that
$v_{p}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v_{p}^{\prime}$. By repeated use of ctx, we find $\texttt{bEq}_{b}\
e_{l}\ e_{r}\ e_{p}\hookrightarrow^{*}\texttt{bEq}_{b}\ e_{l}\ e_{r}\ v_{p}$.
Since its proof part is a value, this term is a value. We find
$\texttt{bEq}_{b}\ e_{l}\ e_{r}\
v_{p}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\texttt{bEq}_{b}\ e_{l}^{\prime}\ e_{r}^{\prime}\ v_{p}^{\prime}$ by
ebeq.

  * •

$v\doteq\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau}\
e_{l}^{\prime}\ e_{r}^{\prime}\ v_{p}^{\prime}$. It must be the case that
$e=\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\ e_{p}$
where $\tau_{x}\rightrightarrows\tau_{x}^{\prime}$ and
$\tau\rightrightarrows\tau^{\prime}$ and $e_{l}\rightrightarrows
e_{l}^{\prime}$ and $e_{r}\rightrightarrows e_{r}^{\prime}$ and
$e_{p}\rightrightarrows v_{p}^{\prime}$. Since parallel reduction implies
reduction to congruent forms (Lemma C.11), we have
$e_{p}\hookrightarrow^{*}e_{p}^{\prime}$ and
$e_{p}^{\prime}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v_{p}^{\prime}$. By the IH on $v_{p}^{\prime}$, we know that
$e_{p}^{\prime}\hookrightarrow^{*}v_{p}$ such that
$v_{p}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v_{p}^{\prime}$. By repeated application of ctx, we find
$\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\
e_{p}\hookrightarrow^{*}\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\
e_{l}\ e_{r}\ v_{p}$. Since its proof part is a value, this term is a value.
We find $\texttt{xEq}_{{\tau_{x}}\text{:}{\tau}\rightarrow\ }e_{l}\ e_{r}\
v_{p}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime}}\
e_{l}^{\prime}\ e_{r}^{\prime}\ v_{p}^{\prime}$ by exeq. ∎

###### Corollary C.13 (Parallel reduction to a value implies reduction to a
related value).

If $e\rightrightarrows v^{\prime}$ then there exists $v$ such that
$e\hookrightarrow^{*}v$ and $v\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v^{\prime}$.

###### Proof.

Since parallel reduction implies reduction to congruent forms (Lemma C.11), we
have $e\hookrightarrow^{*}e^{\prime}$ such that
$e^{\prime}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v^{\prime}$. But congruence to a value implies reduction to a value
(Lemma C.12), so $e^{\prime}\hookrightarrow^{*}v$ such that
$v\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v^{\prime}$. By transitivity of reduction, $e\hookrightarrow^{*}v$. ∎

###### Lemma C.14 (Congruence is a backward simulation).

If $e_{1}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}$ and $e_{2}\hookrightarrow e_{2}^{\prime}$ then there exists
$e_{1}^{\prime}$ where $e_{1}\hookrightarrow^{*}e_{1}^{\prime}$ such that
$e_{1}^{\prime}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}e_{2}^{\prime}$.

###### Proof.

By induction on the derivation of $e_{2}\hookrightarrow e_{2}^{\prime}$.

  * ctx

$\mathcal{E}[e]\hookrightarrow\mathcal{E}[e^{\prime}]$, where
$e\hookrightarrow e^{\prime}$.

    * –

$\mathcal{E}\doteq\bullet$. By the outer IH.

    * –

$\mathcal{E}\doteq\mathcal{E}_{1}\ e_{2}$. It must be that $e_{1}=e_{11}\
e_{12}$, where $e_{11}\rightrightarrows\mathcal{E}_{1}[e]$ and
$e_{12}\rightrightarrows e_{2}$. By the IH on $\mathcal{E}_{1}$, finding
evaluation with ctx and congruence with app.

    * –

$\mathcal{E}\doteq v_{1}^{\prime}\ \mathcal{E}_{2}$. It must be that
$e_{1}=e_{11}\ e_{12}$, where $e_{11}\rightrightarrows v_{1}^{\prime}$ and
$e_{12}\rightrightarrows\mathcal{E}_{2}[e_{2}]$. We find that
$e_{11}\hookrightarrow^{*}v_{1}$ such that
$v_{1}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}v_{1}^{\prime}$ by Corollary C.13. By the IH on $\mathcal{E}_{2}$ and
evaluation with ctx and congruence with app.

    * –

$\mathcal{E}\doteq\texttt{bEq}_{b}\ e_{l}^{\prime}\ e_{r}^{\prime}\
\mathcal{E}^{\prime}$. It must be the case that $e_{1}=\texttt{bEq}_{b}\
e_{l}\ e_{r}\ e_{p}$ where $e_{l}\rightrightarrows e_{l}^{\prime}$ and
$e_{r}\rightrightarrows e_{r}^{\prime}$. By the IH on $\mathcal{E}^{\prime}$;
we find the evaluation with ctx and congruence with beq.

    * –

$\mathcal{E}\doteq\texttt{xEq}_{{x}\text{:}{\tau_{x}^{\prime}}\rightarrow\tau^{\prime}}\
e_{l}^{\prime}\ e_{r}^{\prime}\ \mathcal{E}^{\prime}$. It must be the case
that $e_{1}=\texttt{xEq}_{{x}\text{:}{\tau_{x}}\rightarrow\tau}\ e_{l}\ e_{r}\
e_{p}$ such that $\tau_{x}\rightrightarrows\tau_{x}^{\prime}$ and
$\tau\rightrightarrows\tau^{\prime}$ and $e_{l}\rightrightarrows
e_{l}^{\prime}$ and $e_{r}\rightrightarrows e_{r}^{\prime}$. By the IH on
$\mathcal{E}^{\prime}$; we find the evaluation with ctx and congruence with
xeq.

  * $\beta$

$(\lambda x\mathord{:}\tau^{\prime}.~{}e^{\prime})\ v^{\prime}\hookrightarrow
e^{\prime}[v^{\prime}/x]$. Congruence implies that $e_{1}=e_{11}\ e_{12}$ such
that $e_{11}\rightrightarrows\lambda x\mathord{:}\tau^{\prime}.~{}e^{\prime}$
and $e_{12}\rightrightarrows v^{\prime}$. Parallel reduction to a value
implies reduction to a congruent value (Corollary C.13),
$e_{11}\hookrightarrow^{*}v_{11}$ such that
$v_{11}^{\prime}\mathrel{\leavevmode\hbox{\set@color\hskip
10.0pt\leavevmode\hbox{\set@color\leavevmode\hbox{\set@color\hskip
5.0pt\leavevmode\hbox{\set@color}\raisebox{0.0pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
5.0pt}}\raisebox{-3.77881pt}{\leavevmode\hbox{\set@color$\rightsquigarrow$}}\hskip
10.0pt}}\lambda x\mathord{:}\tau^{\prime}.~{}e^{\prime}$, i.e.,
$v_{11}=\lambda x\mathord{:}\tau.~{}e$ such that
$\tau\rightrightarrows\tau^{\prime}$ and $e\rightrightarrows e^{\prime}$.
Similarly, $e_{12}\hookrightarrow^{*}v$ such that
$v\mathrel{\leavevmode\hbox{\set@color\hskip