* Case $d_\sigma' = \dyn$. Define $\dyn \circ \dyn = \dyn$. Define $\texttt{Inj}(d) \circ \dyn = \texttt{Inj}(d)$.
An concrete effect set cannot be composed with $\dyn$.

* Case $d_\sigma' = \texttt{Inj}(d)$. Note that $\sigma'' = \dyn$.
We define $d_\sigma \circ \texttt{Inj}(d) = \texttt{Inj}(d_\sigma \circ d)$.

* Case $d_\sigma' = d_c'$: Define $(d_c \circ d_c')$ by
$\effarr \effname c d \in (d_c \circ d_c')$ if and only if $c = c_1 \circ c_2$ and $d = d_1 \circ d_2$ with
$\effarr \effname c_1 d_1 \in d_c$ and $\effarr \effname c_2 d_2 \in d_c'$.

Let $c : A \ltdyn B$ and $d_\sigma : \sigma \ltdyn \sigma'$. The following hold.

* $c \circ B = A \circ c = c$.

* $d_\sigma \circ \sigma' = \sigma \circ d_\sigma = d_\sigma$.

Follows from the uniquenes of precision derivations. That is, $c \circ B$, $A \circ c$, and $c$
all are all proofs of $A \ltdyn B$, hence are equal.

Suppose $\effname @ c \leadsto d \in d_\sigma \circ d_\sigma'$.
Then there exist $c_1, c_2$ and $d_1, d_2$ such that
$\effname @ c_1 \leadsto d_1 \in d_\sigma$ and
$\effname @ c_2 \leadsto d_2 \in d_\sigma'$ and
$c = c_1 \circ c_2$ and $d = d_1 \circ d_2$.

By induction on $d_\sigma'$.

* Case $d_\sigma' = \dyn$.
If $d_\sigma = \dyn$, then our assumption becomes $\effname @ c \leadsto d \in \dyn \circ \dyn = \dyn$.
By definition of membership in $\dyn$, this means that $\effname @ c^r \leadsto d^r \in \sig$.

We may take $c_1 = c$ and take $c_2$ to be the reflexivity derivation for $c^r \ltdyn c^r$.
Likewise, we take $d_1 = d$ and $d_2$ to be the relfexivity derivation for $d^r \ltdyn d^r$.
Note that $\effname @ c_2 \leadsto d_2 \in \dyn$, because $c_2^r = c^r$ and $d_2^r = d^r$,
and we know $\effname @ c^r \leadsto d^r \in \sig$.
We also have that
$c = c_1 \circ c_2$ and $d = d_1 \circ d_2$, using Lemma <ref>.

If $d_\sigma = \texttt{inj}(d_\sigma)$, then our assumption becomes
$\effname @ c \leadsto d \in \texttt{inj}(d_\sigma)$. By definition of membership in $\inj{}{}$,
we have that $\effname @ c \leadsto d \in d_\sigma$.
We may again take $c_1 = c$ and $c_2$ to be the reflexivity derivation for $c^r \ltdyn c^r$,
and likewise for $d_1$ and $d_2$. The same reasoning as above applies.

* Case $d_\sigma' = \texttt{inj}(d_\sigma)$.
By definition of composition, our assumption becomes
$\effname @ c \leadsto d \in (d_\sigma \circ \texttt{inj}(d_\sigma)) = \texttt{inj}(d_\sigma \circ d_\sigma)$.

By the induction hypothesis, there are $c_1, c_2$ and $d_1, d_2$ such that
$\effname @ c_1 \leadsto d_1 \in d_\sigma$ and
$\effname @ c_2 \leadsto d_2 \in d_\sigma$ and
$c = c_1 \circ c_2$ and $d = d_1 \circ d_2$.
By definition of membership in $\inj{}{}$, we have
$\effname @ c_2 \leadsto d_2 \in \texttt{inj}(d_\sigma) = d_\sigma'$.

* Case $d_\sigma' = d_c'$ (concrete effect set).
Similar to previous case.

§.§.§ Congruence Rules

With these lemmas, we can prove the soundness of the term precision congruence rules.
The proofs are by induction on the term precision derivation.

We need to show that $\Gamma^{\ltdyn} \vDash_{d_{\sigma}} \sem{\tru} \ltdyn \sem{\tru} \in \boolty$, and likewise for $\fls$ (we will show this for $\tru$ only; the reasoning for $\fls$ is exactly the same.)

Let $\sim \, \in \{<, >\}$ and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} i$. We need to show

\[
\left(\tru[\gamma_1], \tru[\gamma_2]\right) \in
\simierel {d_\sigma} i {\simivrel {\boolty} {}},
\]

\[ \left(\tru, \tru\right) \in \simierel {d_\sigma} i {\simivrel \boolty {}}. \]

By Lemma <ref>, it suffices to show that $(\tru, \tru) \in \simivrel {\boolty} {i}$. This is true according to the definition of the logical relation.

We need to show that $\Gamma^\ltdyn, x_1 \ltdyn x_2 : c, \Gamma'^\ltdyn \vDash_{d_\sigma} x_1 \ltdyn x_2 \in c$.

Let $\sim \, \in \{<, >\}$, and let $\widehat{\Gamma}^\ltdyn = \Gamma^\ltdyn, x_1 \ltdyn x_2 : c, \Gamma'^\ltdyn$. Let $(\gamma_1, \gamma_2) \in \simigrel {\widehat{\Gamma}^\ltdyn} i$. We need to show

\[ \left(x_1[\gamma_1], x_2[\gamma_2]\right) \in \simierel {d_\sigma} i {\simivrel {c} {}}. \]

By Lemma <ref>, it suffices to show that $(\gamma_1(x_1), \gamma_2(x_2)) \in \simivrel c i$. But this follows from the fact that $(\gamma_1, \gamma_2) \in \simigrel {\widehat{\Gamma}^\ltdyn} i$. In particular, by the definition of the logical relation, since $(x_1 \ltdyn x_2 : c) \in \widehat{\Gamma}^\ltdyn$, we have $(\gamma_1(x_1), \gamma_2(x_2)) \in \simivrel c i$.

Suppose $\Gamma^{\ltdyn}, x \ltdyn y : c \vDash_{d_{\sigma'}} {M} \ltdyn {N} \in d$.
We need to show that $\Gamma^{\ltdyn} \vDash_{d_{\sigma}} {\lambda x.M} \ltdyn {\lambda y.N} \in c \to_{d_{\sigma'}} d$.

Let $\sim \, \in \{<, >\}$ and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} i$. We need to show

\[
\left((\lambda x.M)[\gamma_1], (\lambda y.N)[\gamma_2]\right) \in
\simierel {d_\sigma} i {\simivrel {c \to_{d_{\sigma'}} d} {}}.
\]

Let $V_1 = \lambda x.{M}[\gamma_1]$ and $V_2 = \lambda y.{N}[\gamma_2]$.
By Lemma <ref>, it will suffice to show that $(V_1, V_2) \in \simivrel {c \to_{d_{\sigma'}} d} i$. To this end, let $k \le i$ and let $(V_{i1}, V_{i2}) \in \simivrel c k$. We will show that $(V_1\, V_{i1}, V_2\, V_{i2}) \in \simierel {d_{\sigma'}} k {\simivrel d {}}$.

Let $M' = ({M}[\gamma_1])(V_{i1}/x)$ and let $N' = ({N}[\gamma_2])(V_{i2}/y)$. Note that $(V_1\, V_{i1}) \stepsin 1 M'$, and similarly $(V_2\, V_{i2}) \stepsin 1 N'$. Thus, if $k = 0$, then by the Time-out Lemma (Lemma <ref>), we conclude that $(V_1\, V_{i1}, V_2\, V_{i2}) \in \simierel {d_{\sigma'}} k {\simivrel d {}}$.

Hence, from now on, we assume $k \ge 1$. By the Anti-reduction lemma (Lemma <ref>) (with $i_1 = i_2 = 1$ and $j = k$), it will suffice to show that $(M', N') \in \simierel {d_{\sigma'}} {k-1} {\simivrel d {}}$.

This will follow by our inductive hypothesis, which says that for any $\sim \,\in \{<, >\}$, any natrual number $n$, and any $(\gamma_1', \gamma_2') \in \simigrel {\Gamma^\ltdyn, x \ltdyn y : c} n$, we have

\[ ({M}[\gamma_1'], {N}[\gamma_2']) \in \simierel {d_{\sigma'}} {n} {\simivrel {d} {}}. \]

Let $\gamma_1' = \gamma_1, V_{i1}/x$, let $\gamma_2' = \gamma_2, V_{i2}/y$. It is easily verified that $(\gamma_1', \gamma_2') \in \simigrel {\Gamma^\ltdyn, x \ltdyn y : c} {k-1}$. (Doing so requires the monotonicity lemma, combined with the fact that $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} i$ and that $k-1 < k \le i$).

Taking $n = k-1$ above, and noting that $M' = {M}[\gamma_1']$ and $N' = {N}[\gamma_2']$, it follows that $(M', N') \in \simierel {d_{\sigma'}} {k-1} {\simivrel d {}}$, as we wanted to show.

Suppose $\Gamma^{\ltdyn} \vDash_{d_{\sigma}} {M_1} \ltdyn {M_2} \in c \to_{d_{\sigma}} d$, and that $\Gamma^{\ltdyn} \vDash_{d_{\sigma}} {N_1} \ltdyn {N_2} \in c$.

We need to show that $\Gamma^{\ltdyn} \vDash_{d_{\sigma}} {M_1\, N_1} \ltdyn {M_2\, N_2} \in d$.

Let $\sim \, \in \{<, >\}$ and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} i$. We need to show

\[
\left({M_1 \, N_1}[\gamma_1], {M_2 \, N_2}[\gamma_2]\right) \in
\simierel {d_\sigma} i {\simivrel {d} {}}.
\]

By Lemma <ref>, it will suffice to show that

(1) $(M_1[\gamma_1], M_2[\gamma_2]) \in
\simierel {d_\sigma} i {\simivrel {c \to_{d_\sigma} d} {}}$,

and that (2) for all $k \le i$ and
$(V_1, V_2) \in
\simivrel {c \to_{d_\sigma} d} k$,
we have $(V_1\, N_1, V_1\, N_2) \in \simierel {d_\sigma} k {\simivrel {d} {}}$.

(1) follows immediately from our first top-level assumption.

To show (2), we again apply Lemma <ref>. It follows from our second top-level assumption that $(N_1[\gamma_1], N_2[\gamma_2]) \in \simierel {d_\sigma} k {\simivrel c {}}$. Now let $k' \le k$ and $(V_1', V_2') \in \simivrel {c} {k'}$. We claim that

\[
(V_1\, V_1', V_2\, V_2') \in
\simierel {d_\sigma} {k'} {\simivrel {d} {}}.
\]

This holds since $(V_1, V_2) \in \simivrel {c \to_{d_\sigma} d} k$ and
$(V_1', V_2') \in \simivrel {c} {k'}$.

* $\Gamma^{\ltdyn} \vDash_{d_{\sigma}} \sem{M} \ltdyn \sem{M'} \in \boolty$

* $\Gamma^{\ltdyn} \vDash_{d_{\sigma}} \sem{N_t} \ltdyn \sem{N_t'} \in c$

* $\Gamma^{\ltdyn} \vDash_{d_{\sigma}} \sem{N_f} \ltdyn \sem{N_f'} \in c$

Let $\sim \, \in \{<, >\}$ and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} i$. We need to show

\[
\left({\ifXthenYelseZ{M}{N_t}{N_f}}[\gamma_1],
\in \simierel {d_\sigma} i {\simivrel {c} {}}.
\]

By Lemma <ref>, it will suffice to show that
(1) $(\sem{M}[\gamma_1], \sem{M'}[\gamma_2]) \in \simierel {d_\sigma} i {\simivrel {\boolty} {}}$, and
(2) for all $k \le i$ and $(V_1, V_2) \in \simivrel {\boolty} {k}$, we have

\[
(\ifXthenYelseZ {V_1} {{N_t}[\gamma_1]}{{N_f}[\gamma_1]}),
(\ifXthenYelseZ {V_2} {{N_t'}[\gamma_2]}{{N_f'}[\gamma_2]})
\in \simierel {d_\sigma} k {\simivrel {c} {}}.
\]

We note that (1) follows by our first top-level assumption. For (2), the assumption $(V_1, V_2) \in \simivrel {\boolty} {k}$ has two cases. If $V_1 = V_2 = \tru$, then by anti-reduction (Lemma <ref>), it will suffice to show $({{N_t}[\gamma_1]}, {{N_t'}[\gamma_2]}) \in \simierel {d_\sigma} k {\simivrel {c} {}}$. But this follows from our second top-level assumption. Similarly, if $V_1 = V_2 = \fls$, then it suffices to show that $({{N_f}[\gamma_1]}, {{N_f'}[\gamma_2]}) \in \simierel {d_\sigma} k {\simivrel {c} {}}$, which follows from our third top-level assumption.

This proof is similar to the function abstraction proof and is hence omitted.

Let $c : A_1 \ltdyn A_2$ and $d : B_1 \ltdyn B_2$. Suppose $\effname@c \leadsto d \in d_\sigma$ and

\[
\Gamma^\ltdyn \vDash_{d_\sigma} M_1 \ltdyn M_2 \in c.
\]

We need to show that

\[
\Gamma^\ltdyn \vDash_{d_\sigma}
{\raiseOpwithM \effname {M_1}} \ltdyn
{\raiseOpwithM \effname {M_2}} \in d.
\]

Let $\sim\, \in \{<, >\}$ and $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$. We will show

\[
({\raiseOpwithM \effname {M_1}}[\gamma_1],
{\raiseOpwithM \effname {M_2}}[\gamma_2])
\in \simierel {d_\sigma} {j} {\simivrel d {}}.
\]

We apply Lemma <ref>. We first claim that $({M_1}[\gamma_1], {M_2}[\gamma_2]) \in \simierel {d_\sigma} j {\simivrel c {}}$. This follows by assumption. Now, let $k \le j$ and $(V_1, V_2) \in \simivrel c k$. We claim that

\[
({\raiseOpwithM \effname {V_1}}[\gamma_1],
{\raiseOpwithM \effname {V_2}}[\gamma_2])
\in \simierel {d_\sigma} {k} {\simivrel d {}}.
\]

By Lemma <ref>, it suffices to show that

\[
({\raiseOpwithM \effname {V_1}}[\gamma_1],
{\raiseOpwithM \effname {V_2}}[\gamma_2])
\in \simirrel {d_\sigma} {k} {\simivrel d {}}.
\]

We assert the second disjunct in the definition of $\simirrel{\cdot}{}{}$, where we take $\effname$ to be $\effname$ (which we know by assumption is in $d_\sigma$), and we take $E^l = E^r = \hole$ and $V^l = V_1$, $V^r = V_2$.

We need to show that $(V_1, V_2) \in (\later \simivrel{c}{})_k$, and that

\[
( x^l.(\hole [x^l]), x^r.(\hole [x^r]) ) \in
(\later \simikrel {d} {})_k
(\simierel {d_\sigma} {} {\simivrel d {}})
\]

To this end, let $k' \le k$ and let $(V^l, V^r) \in \simivrel {c} {k'}$. We need to show

\[
(V^l, V^r) \in \simierel {d_\sigma} {k'} {\simivrel d {}}.
\]

But this follows by Lemma <ref>.

M M' : d_σ cy:c ⊢N N' : d_τ d

∀@ d_i d_o ∈d_σ.
(∉(ϕ) ∧∉(ϕ') ∧: d_i d_o ∈d_τ) ∨

x:d_i, k : d_o d_τ d ⊢ϕ() ϕ'() : d_τ d

M y N ϕM' y N' ϕ' : d_τ d

We use Löb induction (Lemma <ref>). Assume that for
all $k \le j$ and all $(\gamma_1, \gamma_2) \in (\later \simigrel {\Gamma^\ltdyn} {})_{k}$ and all
$(M, M') \in (\later \simierel {d_\sigma} {} {})_{k} (\simivrel c {})$, we have

\begin{align*} (
&{\hndl M x N \phi}[\gamma_1], \\
&{\hndl {M'} {x'} {N'} {\phi'}}[\gamma_2] )
\\ & \quad \quad \in (\later \simierel {d_{\tau}} j {}_{k} (\simivrel d {}).
\end{align*}

Let $(M, M') \in \simierel {d_\sigma} {j} {\simivrel c {}}$.

Let $\sim\, \in \{<, >\}$ and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} {j}$.
We need to show that

\begin{align*} (
&{\hndl M x N \phi}[\gamma_1], \\
&{\hndl {M'} {x'} {N'} {\phi'}}[\gamma_2] )
\\ & \quad \quad \in \simierel {d_{\tau}} j {\simivrel d {}}.
\end{align*}

By monadic bind (Lemma <ref>), it suffices to consider the following

* Let $k \le j$ and let $(V_1, V_2) \in {\simivrel c {k}}$. We need to show that

\begin{align*} (
&{\hndl {V_1} x {N[\gamma_1]} {\phi[\gamma_1]}}, \\
&{\hndl {V_2} {x'} {N'[\gamma_2]} {\phi'[\gamma_2]}} )
\\ & \quad \quad \in \simierel {d_{\tau}} j {\simivrel d {}}.
\end{align*}

By anti-reduction (Lemma <ref>), it suffices to show that

\[
( N[\gamma_1][V_1/x], N'[\gamma_2][V_2/x'] ) \in
\simierel {d_{\tau}} k {\simivrel d {}}.
\]

This follows from the premise: if we let
$\gamma_1' = \gamma_1, V_1/x$ and $\gamma_2' = \gamma_2, V_2/x'$,
then it is easily checked that
$(\gamma_1', \gamma_2') \in \simigrel {\Gamma^\ltdyn, x \ltdyn x' : c} j$.
Furthermore, $N[\gamma_1][V_1/x] = N[\gamma_1']$ and likewise for
$N[\gamma_2][V_2/x']$. The premise then implies that
$(N[\gamma_1][V_1/x], N'[\gamma_2][V_2/x']) \in \simierel {d_{\tau}} k {\simivrel d {}}$,
as needed.

* Let $k \le j$ and let $\effname @ d_i \leadsto d_o \in d_\sigma$
be an effect that is caught by either handler – i.e., $\effname \in \dom(\phi)$ or
$\effname \in \dom(\phi')$. By the premise, it follows that $\effname$ is in both
$\dom(\phi)$ and $\dom(\phi')$.

Let $(V^l, V^r) \in (\later \simivrel {c_i} {})_k$. Let $E^l \apart \effname$ and
$E^r \apart \effname$ be evaluation contexts such that

\[ (x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_o}{})_k
(\simierel{d_{\sigma}} {} {\simivrel c {}}). \]

We need to show that

\begin{align*} (
&{\hndl {E^l[\raiseOpwithM{\effname}{V^l}} x {N[\gamma_1]} {\phi[\gamma_1]}}, \\
&{\hndl {E^r[\raiseOpwithM{\effname}{V^r}} {x'} {N'[\gamma_2]} {\phi'[\gamma_2]}} )
\\ & \quad \quad \in \simierel {d_{\tau}} k {\simivrel d {}}.
\end{align*}

By anti-reduction, it suffices to show that

\begin{align*}
[(\lambda y.\hndl {E^l[y]} x {N[\gamma_1]} {\phi[\gamma_1]})/k], \\
[(\lambda y.\hndl {E^r[y]} {x'} {N'[\gamma_2]} {\phi'[\gamma_2]})/k']
) \\ & \quad \quad \in (\later \simierel {d_{\tau}} {} {})_{k} (\simivrel d {}).
\end{align*}

To show this, we apply the premise, as follows.
Let $H_1 = \hndl {E^l[y]} x {N[\gamma_1]} {\phi[\gamma_1]}$ and
$H_2 = \hndl {E^r[y]} {x'} {N'[\gamma_2]} {\phi'[\gamma_2]}$. Let
$\gamma_1' = \gamma_1, V^l/x_i,  (\lambda y. H_1)/k_i$ and let
$\gamma_2' = \gamma_2, V^r/x_i', (\lambda y. H_2)/k_i'$.
In order to apply the premise, we must prove that
$(\gamma_1', \gamma_2') \in \simigrel {\Gamma^\ltdyn, x_i \ltdyn x_i' : d_i, k_i \ltdyn k_i' : d_o \to_{d_{\tau}} d} {k'}$.

We first need to show that $(V^l, V^r) \in (\later \simivrel {c_i} {})_{k}$.
This holds by assumption. We now need to show that

\[
( (\lambda y. H_1), (\lambda y. H_2) ) \in
(\later \simivrel {d_o \to_{d_{\tau}} d} {})_{k}.
\]

To this end, let $k' \le k$ and let $(V_A, V_B) \in (\later \simivrel {d_o} {})_{k'}$. We need to show that

\begin{align*}
&(\lambda y. H_1)\, V_A, (\lambda y. H_2)\, V_B )
\\ &\quad \quad \in (\later \simierel {d_{\tau}} {} {})_{k'} (\simivrel d {})
\end{align*}

By anti-reduction, it suffices to show that

\begin{align*}\label{eq:handle_goal_final}
&\hndl {E^l[V_A]} x N {\phi},
\hndl {E^r[V_B]} {x'} {N'} {\phi'}
) \\ & \quad \quad \in (\later \simierel {d_{\tau}} {} {})_{k'} (\simivrel d {}).
\end{align*}

By the Löb induction hypothesis, it will suffice to show that

\begin{align*}
&{E^l[V_A]}, {E^r[V_B]}
) \quad \quad \in (\later \simierel {d_{\sigma}} {} {})_{k'} (\simivrel c {}).
\end{align*}

Recall that by assumption, we have

\[ (x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_o}{})_k
(\simierel{d_{\sigma}} {} {\simivrel c {}}). \]

Thus, it suffices to show that $(V_A, V_B) \in (\later \simivrel {d_o} {})_{k'}$,
which is precisely our assumption.

Note that we do not need to show soundness of the term precision congruence rules involving casts.
This will follow from the soundness of the upper and lower bound rules for casts.

Let $M$ be a term such that $\hastyRhoMT{\sigma}{M}{A}$. We have
$\sg^\ltdyn \vDash_\sigma M \ltdyn M : A$.

By induction on $M$, using the soundness of the term precision relation already proven.

§.§.§ Equational Rules

x_1 x_2 : c _d_σ M ≡N : d V ≡V' : c
M[V/x_1] ≡N[V'/x_2]

Suppose for all $j$ and all $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn, x^l \ltdyn x^r : c} {j}$, that

\[
(x_1.M, x_2.N) \in \simierel {d_\sigma} {j} {\simivrel {d} {}}
\]

\[
(x_2.N, x_1.M) \in \simierel {d_\sigma} {j} {\simivrel {d} {}}.
\]

Further suppose that for all $j$,

\[(V, V') \in \simivrel {c} {j} \]

\[(V', V) \in \simivrel {c} {j}. \]

Let $j$ be arbitrary, and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} {}$.
We need to show

\[
(M[V/x_1], N[V'/x_2]) \in \simierel {d_\sigma} {j} {\simivrel {d} {}}
\]

\[
(N[V'/x_2], M[V/x_1]) \in \simierel {d_\sigma} {j} {\simivrel {d} {}}.
\]

The second statement is symmetric to the first, so we show only the first.

Let $\gamma_1' = (\gamma_1, x_1 = V)$ and let $\gamma_2' = (\gamma_2, x_2 = V')$.

Note that we have $M[\gamma_1'] = M[\gamma_1][V/x_1]$ and $N[\gamma_2'] = N[\gamma_2][V'/x_2]$,
by definition of substitution.

By our assumption, it is sufficient to show that $(\gamma_1', \gamma_2') \in
\simigrel {\Gamma^\ltdyn, x_1 \ltdyn x_2 : c} {j}$.

For this, it sufficies to show that
$(\gamma_1'(x_1), \gamma_2'(x_2)) \in \simivrel {c} {j}$. But $\gamma_1'(x_1) = V$ and
$\gamma_2'(x_2) V'$, so we are finished.

*[]y x N ≡N[y/x]

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(\letXbeboundtoYinZ{y}{x}{N}, N[y/x]) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

Since $y$ is a variable and hence a value, we have by the operational semantics that

\[ \letXbeboundtoYinZ{y}{x}{N} \stepsin 1 N[y/x]. \]

Thus, by anti-reduction, it suffices to show that

\[
(N[y/x], N[y/x]) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

But this follows by reflexivity (Corollary <ref>).

*[]M x x ≡M

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(\letXbeboundtoYinZ M x x, M) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

Since $x$ is a variable and hence a value, we have by the operational semantics that

\[\letXbeboundtoYinZ{M}{x}{x} \stepsin 1 M[x/x]. \]

By definition of substitution, $M[x/x] = M$. Thus, by anti-reduction, it suffices
to show that

\[
(M, M) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

This follows by reflexivity (Corollary <ref>).

(M x N) y P ≡M x N y P

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(\letXbeboundtoYinZ {(\letXbeboundtoYinZ M x N)} y P,
\letXbeboundtoYinZ M x \letXbeboundtoYinZ N y P) \in
\simierel {\sigma} {j} {\simivrel {B} {}}.
\]

We apply Lemma <ref>, taking
$E_1 = \letXbeboundtoYinZ {(\letXbeboundtoYinZ{\hole}{x}{N})} {y} {P}$ and
$E_2 = \letXbeboundtoYinZ {\hole} {x} {\letXbeboundtoYinZ N y P}$.

We first need to show that $(M, M) \in \simierel {\sigma} {j} {\simivrel {A} {}}$,
which is true by reflexivity (Corolarry <ref>).

Now, let $k \le j$ and $(V_1, V_2) \in \simivrel {A} {k}$. We need to show that

\[
\letXbeboundtoYinZ {(\letXbeboundtoYinZ{V_1}{x}{N})} {y} {P},
\letXbeboundtoYinZ {V_2} {x} {\letXbeboundtoYinZ N y P}
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

According to the operational semantics, we have

\[ (\letXbeboundtoYinZ{V_1}{x}{N}) \stepsin 1 N[V_1/x]. \]

\[
\letXbeboundtoYinZ {(\letXbeboundtoYinZ{V_1}{x}{N})} {y} {P} \stepsin 1
\letXbeboundtoYinZ {N[V_1/x]} {y} {P}.
\]

Similarly, we have

\[ \letXbeboundtoYinZ {V_2} {x} {\letXbeboundtoYinZ N y P}
\stepsin 1 (\letXbeboundtoYinZ N y P)[V_2/x]
= \letXbeboundtoYinZ {N[V_2/x]} {y} {P[V_2/x]}. % TODO is this correct?
\]

Note that since $x$ does not occur in $P$, we have $P[V_2/x] = P$.

Now, by anti-reduction, it suffices to show

\[
\letXbeboundtoYinZ {N[V_1/x]} {y} {P},
\letXbeboundtoYinZ {N[V_2/x]} {y} {P}
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

We again apply Lemma <ref>, this time with
$E_1 = \letXbeboundtoYinZ {\hole} {y} {P}$ and
$E_2 = \letXbeboundtoYinZ {\hole} {y} {P}$.

We first need to show that
$(N[V_1/x], N[V_2/x]) \in \simierel {\sigma} {k} {\simivrel {A} {}}$.
This follows from reflexivity (Corollary <ref>) and
value substitution (Lemma <ref>) applied to our assumption
on $V_1$ and $V_2$.

Now let $k' \le k$ and $(V_1', V_2') \in \simivrel {k'} {A}$. We need to show that

\[
( \letXbeboundtoYinZ {V_1'} {y} {P},
\letXbeboundtoYinZ {V_2'} {y} {P}
) \in \simierel {\sigma} {k'} {\simivrel {B} {}}.
\]

By anti-reduction, it suffices to show

\[ (P[V_1'/y], P[V_2'/y]) \in \simierel {\sigma} {k'} {\simivrel {B} {}}. \]

This again follows from reflexiviy and value substitution.

*[]M[x : ] ≡x M[/x]M[/x]

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma, x_1 \ltdyn x_2 : \boolty} {j}$.
We need to show

\[
( M[\gamma_1], (\ifXthenYelseZ x {M[\tru/x]}{M[{\fls/x}]})[\gamma_2] ) \in
\simierel {\sigma} {j} {\simivrel {B} {}}.
\]

By definition of substitution, this is equivalent to

\[
( M[\gamma_1],
(\ifXthenYelseZ \gamma_2(x) {M[\tru/x][\gamma_2]}{M[{\fls/x}][\gamma_2]}) ) \in
\simierel {\sigma} {j} {\simivrel {B} {}}.
\]

By our assumption on $\gamma_1$ and $\gamma_2$, we have that either
$\gamma_1(x_1) = \gamma_2(x_2) = \tru$ or $\gamma_1(x_1) = \gamma_2(x_2) = \fls$.

We show only the former case; the latter is symmetric.
In the former case, we need to show

\[
( M[\tru/x][\gamma_1],
(\ifXthenYelseZ \tru {M[\tru/x][\gamma_2]}{M[{\fls/x}][\gamma_2]})
) \in
\simierel {\sigma} {j} {\simivrel {B} {}}.
\]

By anti-reduction, it is sufficient to show

\[
( M[\tru/x][\gamma_1], M[\tru/x][\gamma_2]
) \in
\simierel {\sigma} {j} {\simivrel {B} {}}.
\]

This follows by reflexivity.

*[]N_tN_f ≡N_t

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
( (\ifXthenYelseZ {\tru} {N_t} {N_f})[\gamma_1], N_t[\gamma_2] ) \in
\simierel {\sigma} {j} {\simivrel {B} {}}.
\]

By anti-reduction, it suffices to show

\[
( N_t[\gamma_1], N_t[\gamma_2] ) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

This holds by reflexivity.

*[]N_tN_f ≡N_f

Precisely dual to the above proof.

*[Right=IfEval]M N_tN_f ≡M x x N_t N_f

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(\ifXthenYelseZ {M} {N_t}{N_f})[\gamma_1],
(\letXbeboundtoYinZ M x \ifXthenYelseZ x {N_t} {N_f})[\gamma_2]
) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

We apply Lemma <ref>, with
$E_1 = \ifXthenYelseZ {\hole} {N_t[\gamma_1]} {N_f[\gamma_1]}$ and
$E_2 = \letXbeboundtoYinZ {\hole} {x} {\ifXthenYelseZ {\gamma_2(x)} {N_t[\gamma_2]} {N_f[\gamma_2]}}$.

We first need to show that $(M[\gamma_1], M[\gamma_2]) \in \simierel {\tau} {j} {\simivrel {\boolty} {}}$.
This follows by reflexivity (Corollary <ref>).

Now let $k \le j$ and let $(V_1, V_2) \in \simivrel {\boolty} {k}$. We need to show that

\[
(\letXbeboundtoYinZ {V_2} {x} {\ifXthenYelseZ {\gamma_2(x)} {N_t[\gamma_2]} {N_f[\gamma_2]}})
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

By definition of $\simivrel {\boolty} {}$, either $V_1 = V_2 = \tru$ or $V_1 = V_2 = \fls$.
We consider the first case; the second is symmetric.

We need to show

\[
(\letXbeboundtoYinZ {\tru} {x} {\ifXthenYelseZ {\gamma_2(x)} {N_t[\gamma_2]} {N_f[\gamma_2]}})
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

By anti-reduction, it suffices to show

\[
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

This follows by reflexivity.

*[Right=FunBeta](λx. M) V ≡M[V/x]

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
((\lambda x. M)\, V)[\gamma_1],
) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

Since $V$ is a value, it suffices by anti-reduction to show that

\[
( M[V/x][\gamma_1], M[V/x][\gamma_2] )
\in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

This follows by reflexivity.

Let $V_f$ be a value such that $\hastyRhoMT{\emptyset}{V}{A \to_{\sigma'} B}$. We have
$\sg^\ltdyn \vDash_\sigma V_f \equiv (\lambda x. V_f x) : (A \to_{\sigma'} B)$.

Let $j$ be arbitrary. We need to show

\[
( V_f, (\lambda x. V_f x) ) \in
\simierel {\emptyset} {j} {\simivrel {A \to_{\sigma'} B} {}}.
\]

As these are values, it suffices by Lemma <ref> to show that they
are related in $\simivrel {A \to_{\sigma'} B} {j}$.
To this end, let $k \le j$ and let $(V_{i1}, V_{i2}) \in \simivrel {A} {k}$. We claim that

\[
( V_f\, V_{i1}, (\lambda x. V_f x)\, V_{i2} ) \in
\simierel {\sigma'} {k} {\simivrel {B} {}}.
\]

By anti-reduction, it will suffice to show that

\[
( V_f\, V_{i1}, V_f\, V_{i2} ) \in
\simierel {\sigma'} {k} {\simivrel {B} {}}.
\]

By reflexivity (Corollary <ref>), we know that $(V_f, V_f) \in \simierel {\emptyset} {k} {A \to_{\sigma'} B}$,
and since $V_f$ is a value, this means that $(V_f, V_f) \in \simivrel {A \to_{\sigma'} B} {k}$.
This immediately implies the desired result, since $(V_{i1}, V_{i2}) \in \simivrel {A} {k}$.

*[]M N ≡M x N y x y

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(M\, N)[\gamma_1],
(\letXbeboundtoYinZ M x \letXbeboundtoYinZ N y x\,y)[\gamma_2]
) \in \simierel {\tau_A} {j} {\simivrel {A_o} {}}.
\]

We apply Lemma <ref>, with $E_1 = (\hole \, N[\gamma_2])$ and
$E_2 = \letXbeboundtoYinZ \hole x \letXbeboundtoYinZ {N[\gamma_2]} y x\,y$.

We first need to show that
$(M[\gamma_1], M[\gamma_2]) \in \simierel {\tau} {j} {\simivrel {A_i \to_{\tau_A} A_o} {}}$.
This follows by reflexivity.

Now let $k \le j$ and let $(V_1, V_2) \in \simivrel {A_i \to_{\sigma_A} A_o} {k}$.
We need to show that

\[
(V_1\, N[\gamma_1]),
(\letXbeboundtoYinZ {V_2} x \letXbeboundtoYinZ {N[\gamma_2]} y x\,y)
) \in \simierel {\tau_A} {k} {\simivrel {A_o} {}}.
\]

By anti-reduction, it suffices to show

\[
(V_1\, N[\gamma_1]),
(\letXbeboundtoYinZ {N[\gamma_2]} y V_2\,y)
) \in \simierel {\tau_A} {k} {\simivrel {A_o} {}}.
\]

We again apply Lemma <ref>, this time with
$E_1 = (V_1\, \hole)$ and $E_2 = \letXbeboundtoYinZ {\hole} {y} {V_2\, y}$.

We need to show  $(N[\gamma_1], N[\gamma_2]) \in \simierel {\tau} {k} {\simivrel {A_i} {}}$,
which holds by reflexivity. Now let $k' \le k$ and let $(V_1', V_2') \in \simivrel {A_i} {k'}$.
We need to show that

\[
(V_1\, V_1'),
(\letXbeboundtoYinZ {V_2'} y V_2\,y)
) \in \simierel {\tau_A} {k'} {\simivrel {A_o} {}}.
\]

By anti-reduction, it suffices to show

\[
(V_1\, V_1'),
(V_2\, V_2')
) \in \simierel {\tau_A} {k'} {\simivrel {A_o} {}}.
\]

This follows from our assumptions on $V_1$ and $V_2$ and on $V_1'$ and $V_2'$.

*[]x y M ϕ≡M[x/y]

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(\hndl x y M \phi)[\gamma_1],
) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

Since $x$ is a value, the above handle term steps, and by anti-reduction it is sufficient to show

\[
) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

This follows by reflexivity.

(x o N_k) y M ϕ≡ϕ()[λo. N_k y M ϕ/k]

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\begin{align*}
& (\hndl {({\letXbeboundtoYinZ {\raiseOpwithM \effname x} o {N_k}})} y M \phi)[\gamma_1], \\
& (\phi(\effname)[\lambda o. \hndl {N_k} y M \phi /k])[\gamma_2]
) \\ & \quad\quad \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\end{align*}

Let $E = \letXbeboundtoYinZ {\hole} {o} {N_k[\gamma_1]}$. Our goal is to show

\begin{align*}
& (\hndl {E[\raiseOpwithM{\effname}{x}]} y {M[\gamma_1]} {\phi[\gamma_1]}), \\
& (\phi(\effname)
[\gamma_2][\lambda o . \hndl
{N_k[\gamma_2]} y {M[\gamma_2]} {\phi[\gamma_2]} /k])
) \\ & \quad\quad \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\end{align*}

Note that $E \apart \effname$. By anti-reduction, it suffices to show

\begin{align*}
& (\phi(\effname)[\gamma_1]
[\lambda o' . \hndl
{E[o']} {y} {M[\gamma_1]} {\phi[\gamma_1]} / k]), \\
& (\phi(\effname)[\gamma_2]
[\lambda o . \hndl
{N_k[\gamma_2]} y {M[\gamma_2]} {\phi[\gamma_2]} / k])
) \\ & \quad\quad \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\end{align*}

That is, we need to show

\begin{align*}
& (\phi(\effname)[\gamma_1]
[\lambda o' . \hndl
{\letXbeboundtoYinZ {o'} {o} {N_k[\gamma_1]}}
{y} {M[\gamma_1]} {\phi[\gamma_1]} / k]), \\
& (\phi(\effname)[\gamma_2]
[\lambda o . \hndl {N_k[\gamma_2]} y {M[\gamma_2]} {\phi[\gamma_2]} / k])
) \\ & \quad\quad \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\end{align*}

By ValSubst, it suffices to show (1)
for all related $(V_{f1}, V_{f2}) \in \simivrel {A_i \to_{\sigma} B} {j}$ and
$\gamma_1' = \gamma_1, V_{f1}/k$ and $\gamma_2' = \gamma_2, V_{f2}/k$, we have

\[
\phi(\effname)[\gamma_1'],
\phi(\effname)[\gamma_2']
) \in \simierel {\sigma} {j} {\simivrel {B} {}},
\]

and (2),

\begin{align*}
& (\lambda o' . \hndl
{\letXbeboundtoYinZ {o'} {o} {N_k[\gamma_1]}}
{y} {M[\gamma_1]} {\phi[\gamma_1]}), \\
& (\lambda o . \hndl {N_k[\gamma_2]} y {M[\gamma_2]} {\phi[\gamma_2]})
) \\ & \quad\quad \in \simierel {\sigma} {j} {\simivrel {A_i \to_{\sigma} B} {}}.
\end{align*}

(1) follows from relfexivity. To show (2), we will use transitivity
(Lemma <ref>).
If $\sim$ is $<$, then note that by MonadUnitL we have

\[ (\letXbeboundtoYinZ{o'}{o}{N_k[\gamma_1]}, N_k[\gamma_2][o'/o]) \in
\simierel {\sigma} {j} {\simivrel {B} {}}, \]

and by soundness of the congruence rules we have

\begin{align*}
& (\lambda o' . \hndl
{\letXbeboundtoYinZ {o'} {o} {N_k[\gamma_1]}}
{y} {M[\gamma_1]} {\phi[\gamma_1]}), \\
& (\lambda o' . \hndl
{y} {M[\gamma_2]} {\phi[\gamma_2]})
) \\ & \quad\quad \in \simierel {\sigma} {j} {\simivrel {A_i \to_{\sigma} B} {}}.
\end{align*}

Then by transitivity, it will suffice to show that

\begin{align*}
& (\lambda o' . \hndl
{y} {M[\gamma_2]} {\phi[\gamma_2]}), \\
& (\lambda o . \hndl
{N_k[\gamma_2]} y {M[\gamma_2]} {\phi[\gamma_2]})
) \\ & \quad\quad \in \simierel {\sigma} {\omega} {\simivrel {A_i \to_{\sigma} B} {}}.
\end{align*}

By congruence for lambdas, it suffices to show that, given related values
$(V_1, V_2) \in \simivrel {A_i} {\omega}$, we have

\begin{align*}
& (\hndl
{N_k[\gamma_2][o'/o][V_1/o']} {y} {M[\gamma_2]} {\phi[\gamma_2]}), \\
& (\hndl {N_k[\gamma_2][V_2/o]} y {M[\gamma_2]} {\phi[\gamma_2]})
) \\ & \quad\quad \in \simierel {\sigma} {\omega} {\simivrel {A_i \to_{\sigma} B} {}}.
\end{align*}

This follows from the soundness of the congruence rules.

On the other hand, if $\sim$ is $>$, then similarly by MonadUnitL we have

\[ (\letXbeboundtoYinZ{o'}{o}{N_k[\gamma_1]}, N_k[\gamma_1][o'/o]) \in
\simierel {\sigma} {\omega} {\simivrel {B} {}}. \]

It then suffices to show that

\begin{align*}
& (\lambda o' . \hndl
{y} {M[\gamma_1]} {\phi[\gamma_1]}), \\
& (\lambda o . \hndl
{N_k[\gamma_2]} y {M[\gamma_2]} {\phi[\gamma_2]})
) \\ & \quad\quad \in \simierel {\sigma} {j} {\simivrel {A_i \to_{\sigma} B} {}},
\end{align*}

which again follows from the soundness of the congruence rules.

M ≡M x x

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(\raiseOpwithM \effname M)[\gamma_1], \,
(\letXbeboundtoYinZ M x \raiseOpwithM \effname x)[\gamma_2]
) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

We apply Monadic Bind (Lemma <ref>), with
$E_1 = \raiseOpwithM {\effname} {\hole}$ and
$E_2 = \letXbeboundtoYinZ {\hole} {x} {\raiseOpwithM \effname x}$.

We first need to show that $(M[\gamma_1], M[\gamma_2]) \in \simierel {\tau} {j} {\simivrel {A} {}}$.
This follows from reflexivity (Corollary <ref>).

Now let $k \le j$ and let $(V_1, V_2) \in \simivrel {A} {k}$. We need to show that

\[
(\raiseOpwithM \effname {V_1})[\gamma_1], \,
(\letXbeboundtoYinZ {V_2} x \raiseOpwithM \effname x)[\gamma_2]
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

As $V_2$ is a value, the above let term steps. By anti-reduction, it suffices to show

\[
(\raiseOpwithM \effname {V_1}), \,
(\raiseOpwithM \effname {V_2})
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

This follows from our assumption on $V_1$ and $V_2$ and
the soundness of the term congruence rule for raise (Lemma <ref>).

M : σB (ϕ_σ) = (σ) ∀∈σ.  x,k⊢ϕ_σ() = k(x)
M ≡M y y ϕ_σ : σB

The proof is by Löb-induction. That is, we suppose that for all $m$,
$(M', N') \in (\later^m \simierel {\sigma} {})_j {\simivrel {A} {}}$ implies that

\begin{align*}
(M', &\hndl {N'}{x}{x}{\phi_\sigma}) \\
&\in (\later^m \simierel {\sigma} {})_j {\simivrel {A} {}}.
\end{align*}

Let $\sim\, \in \{<, >\}$ and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We claim that

\begin{align*}
( M[\gamma_1]&,
(\hndl{N}{x}{x}{\phi_\sigma})[\gamma_2] ) \\
&\in \simierel {\sigma} {j} {\simivrel {A} {}}.
\end{align*}

By monadic bind (Lemma <ref>), it suffices to consider the
following cases:

* Let $k \le j$ and let $(V_1, V_2) \in \simivrel {A} {k}$. We need to show

\begin{align*}
( & V_1, \hndl{V_2}{x}{x[\gamma_2]}{\phi_\sigma} )
\\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

By anti-reduction, it suffices to show that

\[
( V_1, x[\gamma_2][V_2/x] ) \in
\simierel {\sigma} {k} {\simivrel {A} {}},
\]

i.e., $( V_1, V_2 ) \in \simierel {\sigma} {k} {\simivrel {A} {}}$.
Since $V_1$ and $V_2$ are values, it suffices by Lemma <ref>
to show that $(V_1, V_2) \in \simivrel {A} {k}$, which is precisely what we assumed.

* Let $k \le j$ and let $\effname$ be such that $E_2$ catches $\effname$
($E_1$ does not catch anything), i.e., $\effname = \effname_i$ for some $i \in I$.
Let $(V^l, V^r) \in (\later \simivrel {c_i} {})_k$, and let $E^l \apart \effname$
and $E^r \apart \effname$ such that $(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_i}{})_k
(\simierel{\sigma} {} {\simivrel {A} {}})$.

We claim that

\begin{align*} (
&E^l[\raiseOpwithM{\effname}{V^l}], \\
&\hndl {E^r[\raiseOpwithM{\effname}{V^r}]} {x} {x} {\phi_\sigma} ) \\
&\quad \quad \in \simierel {\sigma} k {\simivrel {A} {}}.
\end{align*}

It suffices by anti-reduction to show

\begin{align*} (
Q\, (\raiseOpwithM{\effname}{V^r})
\in \simierel {\sigma} k {\simivrel {A} {}},
\end{align*}

where $Q = (\lambda y. \hndl{E^r[y]}{x}{x}{\phi_\sigma}))$.

The above terms do not step, so it suffices to show they are related in $\simirrel {\sigma} k {\simivrel {A} {}}$.

We assert the second disjunct, taking $V^l = V^l$, $V^r = V^r$, $E^l = E^l$, and $E^r = (Q\, \hole)$.
(Note that the latter context is apart from $\effname$ because $Q$ is a value). We must show that

\[
( x^l.E^l[x^l], x^r.(Q\, \hole)[x^r] ) \in
(\later \simikrel{d_i}{})_k
(\simierel{\sigma} {} {\simivrel {A} {}}).
\]

Let $(V_1, V_2) \in (\later \simivrel {d_i} {})_k$. We claim that

\begin{align*}
( &E^l[V_1],
\hndl{E^r[V_2]}{x}{x}{\phi_\sigma} ) \\
& \quad \quad \in (\later \simierel {\sigma} {})_k {\simivrel {A} {}}.
\end{align*}

By the Löb induction hypothesis, it will suffice to show that

\begin{align*}
( &E^l[V_1], E^r[V_2] ) \\
& \quad \quad \in (\later \simierel {\sigma} {})_k {\simivrel {A} {}}.
\end{align*}

This follows from the assumption that $(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_i}{})_k (\simierel{\sigma} {} {\simivrel {A} {}})$
and the assumption that
$(V_1, V_2) \in (\later \simivrel {d_i} {})_k$.

M x N ∅ ≡M x N

We show one direction of the equivalence; the other is symmetric.

Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\begin{align*}
&(\hndl M x N {\emptyset})[\gamma_1], \\
&(\letXbeboundtoYinZ M x N)[\gamma_2]
) \\ & \quad \quad \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\end{align*}

By Monadic Bind (Lemma <ref>) and the fact that
neither evaluation context catches any effects, it suffices to show that

\begin{align*}
&\hndl {V_1} x {N[\gamma_1]} {\emptyset}, \\
&\letXbeboundtoYinZ {V_2} x N[\gamma_2]
) \\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {B} {}},
\end{align*}

where $k \le j$ and $(V_1, V_2) \in \simivrel {B} {k}$.
By anti-reduction, it will suffice to show that

\begin{align*}
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\end{align*}

Using ValSubst, the result follows by reflexivity and our assumption on $V_1$ and $V_2$.

∀∈(ϕ).  ψ() = ϕ()
∀∈(ψ). ∉(ϕ) ⇒ψ() = k(x)

M y N ϕ≡M y N ψ: σB

We show one direction of the equivalence; the other is symmetric.

The proof is by Löb induction. We assume that

\[
(\hndl M_1' y N \phi)[\gamma_1],
(\hndl M_2' y N \psi)[\gamma_2]
) \in (\later \simierel {\sigma} {} {})_{j} (\simivrel {B} {}).
\]

for all $k \le j$, $(\gamma_1, \gamma_2) \in (\later \simigrel {\Gamma} {})_{k}$ and
$(M_1', M_2') \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {})$.

Let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(\hndl M_1 y N \phi)[\gamma_1],
(\hndl M_2 y N \psi)[\gamma_2]
) \in \simierel {\sigma} {j} {\simivrel {B} {}}
\]

for all $(M_1, M_2) \in \simierel {\sigma} {j} {\simivrel {A} {}}$.

We apply Monadic Bind (Lemma <ref>).
It suffices to consider the following cases:

* Let $k \le j$ and $(V_1, V_2) \in \simivrel {A} {k}$. We need to show that

\[
(\hndl {V_1} y {N[\gamma_1]} {\phi[\gamma_1]}),
(\hndl {V_2} y {N[\gamma_2]} {\psi[\gamma_2]})
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

This follows by anti-reduction and reflexivity.

* Let $k \le j$ and let $\effname \in \sigma$ be an effect caught by either handler,
i.e., $\effname$ is in $\dom(\phi)$ or $\dom(\psi)$.
Let $(V^l, V^r) \in (\later \simivrel {c_\effname} {})_{k}$, and let $E^l \apart \effname$
and $E^r \apart \effname$ such that
$(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_\effname}{})_{k} (\simierel {\sigma} {} {\simivrel {B} {}})$.

We need to show

\begin{align*}
&(\hndl {E^l[\raiseOpwithM{\effname}{V^l}]} y {N[\gamma_1]} {\phi[\gamma_1]}), \\
&(\hndl {E^r[\raiseOpwithM{\effname}{V^r}]} y {N[\gamma_2]} {\psi[\gamma_2]})
) \\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\end{align*}

If $\effname \in \dom(\phi)$, then by the premise, we have
$\psi(\effname) = \phi(\effname)$, so both sides step, and it
suffices by anti-reduction to show

\begin{align*}
& \phi(\effname)[\gamma_1][V^l/x][(\lambda z. \hndl {E^l[z]} y {N[\gamma_1]} {\phi[\gamma_1]}) / k], \\
& \phi(\effname)[\gamma_2][V^r/x][(\lambda z. \hndl {E^r[z]} y {N[\gamma_2]} {\psi[\gamma_2]}) / k]
) \\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {B} {}).
\end{align*}

By ValSubst, it suffices to show that $(V^l, V^r) \in (\later \simivrel {c_\effname} {})_{k}$,
which is true by assumption, and that

\begin{align*}
& (\lambda z. \hndl {E^l[z]} y {N[\gamma_1]} {\phi[\gamma_1]}), \\
& (\lambda z. \hndl {E^r[z]} y {N[\gamma_2]} {\psi[\gamma_2]})
) \\ & \quad \quad \in (\later \simivrel {d_\effname \to_{\sigma} B} {})_{k}.
\end{align*}

By congruence for lambdas, it suffices to show that, given values
$(V_1, V_2) \in (\later \simivrel {d_\effname} {})_{k}$, we have

\begin{align*}
& \hndl {E^l[V_1]} y {N[\gamma_1]} {\phi[\gamma_1]}, \\
& \hndl {E^r[V_2]} y {N[\gamma_2]} {\psi[\gamma_2]}
) \\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {B} {}).
\end{align*}

This follows by the Löb induction hypothesis and our assumption on
$E^l$ and $E^r$.

Now assume that $\effname \notin \dom(\phi)$. Then note that the first handle term
does not step, while the second handle term steps to

\[ \psi(\effname)[\gamma_2][V^r/x][(\lambda z. \hndl {E^r[z]} y {N[\gamma_2]} {\psi[\gamma_2]}) / k]. \]

By the premise, we have $\psi(\effname) = k(\raiseOpwithM \effname x)$.
Thus, by anti-reduction, it suffices to show

\begin{align*}
&(\hndl {E^l[\raiseOpwithM{\effname}{V^l}]} y {N[\gamma_1]} {\phi[\gamma_1]}), \\
& (k(\raiseOpwithM \effname x)[\gamma_2)[V^r/x][(\lambda z. \hndl {E^r[z]} y {N[\gamma_2]} {\psi[\gamma_2]}) / k]
) \\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\end{align*}

That is, it will suffice to show

\begin{align*}
&(\hndl {E^l[\raiseOpwithM{\effname}{V^l}]} y {N[\gamma_1]} {\phi[\gamma_1]}), \\
& ((\lambda z. \hndl {E^r[z]} y {N[\gamma_2]} {\psi[\gamma_2]})\, (\raiseOpwithM \effname V^r))
) \\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\end{align*}

Neither term steps, so it suffices to show they are related
in $\simirrel {\sigma} {k} {\simivrel {B} {}}$.

We need to show that $(V^l, V^r) \in (\later \simivrel {c_\effname} {})_{k}$,
which is true by assumption, and that given $k' \le k$ and related values
$(V_1, V_2) \in (\later \simivrel {d_\effname} {})_{k'}$, we have

\begin{align*}
&(\hndl {E^l[V_1]} y {N[\gamma_1]} {\phi[\gamma_1]}), \\
& ((\lambda z. \hndl {E^r[z]} y {N[\gamma_2]} {\psi[\gamma_2]})\, V_2)
) \\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k'} (\simivrel {B} {}).
\end{align*}

By anti-reduction, it suffices to show

\begin{align*}
&(\hndl {E^l[V_1]} y {N[\gamma_1]} {\phi[\gamma_1]}), \\
&(\hndl {E^r[V_2]} y {N[\gamma_2]} {\psi[\gamma_2]})
) \\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k'} (\simivrel {B} {}).
\end{align*}

This follows by the Löb induction hypothesis and our assumption on $E^l$ and $E^r$.

§.§.§ Cast, Error, and Subtyping Properties

M : d_σ^r c^r
M : d_σ c

Let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} {j}$. We need to show

\[
(\err[\gamma_1], M[\gamma_2]) \in
\simierel {d_\sigma} {j} {\simivrel {c} {}}.
\]

This follows from the definition of the logical relation:
If $\sim$ is $<$ (counting steps on the left), then we are finished by
the definition of the $\ltierel{}{}{}$ relation, because $\err \stepsin 0 \err$.

If $\sim$ is $>$ (counting steps on the right), then we are similarly
finished, because $M \stepsin 0 M$ and the left-hand term is $\err$.

$E[\err] \equiv \err$

We show one direction of the equivalence; the other is symmetric.
Let $j$, $d_\sigma$, and $c$ be arbitrary. We need to show

\[
(E[\err], \err) \in \simierel {d_\sigma} {j} {\simivrel {c} {}}.
\]

By anti-reduction, it is sufficient to show

\[
(\err, \err) \in \simierel {d_\sigma} {j} {\simivrel {c} {}},
\]

which is easily seen to hold by definition of the logical relation.

If $c \subty d$ then $\Vrel c \subseteq \Vrel d$

Further, if $R \subseteq S$ then $\Krel d R \subseteq \Krel c S$,

Further, if $c_\sigma \subty d_\sigma$ then both

* $\Erel{c} R \subseteq \Erel{d} S$

* $\Rrel{c} R \subseteq \Rrel{d} S$

By mutual induction on the subtyping proofs.
First the type subtyping cases:

* $\boolty \subty \boolty$: trivial.

* $c_i \to_{c_e} c_o \subty d_i to_{d_e} d_o$.  Assume
$(V_f,V_f') \in \Vrel{c_i \to_{c_e} c_o}$, we need to show
$(V_f,V_f') \in \Vrel{d_i \to_{d_e} d_o}$.  Let $(V_i,V_i') \in
\Vrel{d_i}$. Then by inductive hypothesis, $(V_i, V_i')\in
\Vrel{c_i}$. Therefore $(V_f V_i, V_f' V_i') \in \Erel{c_e}
\Vrel{c_o}$ and the result follows by the two inductive

The $\Krel{\cdot}$ case follows by a similar argument to the
function case.

The $\Erel{\cdot}$ case follows by inductive hypothesis.

Next the $\Rrel{\cdot}$ cases:

* $\dyn \subty \dyn$: trivial

* $\inferrule{c \subty \sig}{c \subty \dyn}$: trivial by definition of $\Rrel{\dyn}$

* $\inferrule{c \subty d}{c \subty Inj(d)}$: trivial by definition of $\Rrel{Inj(i,d)}$

* $\inferrule{c \subty d}{Inj(c) \subty Inj(d)}$: trivial by definition of $\Rrel{Inj(i,d)}$

* $\inferrule
{\dom(d_c) \subseteq \dom(d'_c) \\\\
\forall \effarr \effname c d \in d_c.
\effarr \effname {c'} {d'} \in d'_c \wedge
c \subty c' \wedge d' \subty d}
{d_c \subty d'_c}$:
Follows using Löb induction by the monotonicity of subtyping for the $\simivrel{\cdot}{}$ and
$\simikrel{\cdot}{}$ relations.

We next prove generalized versions of the cast properties ValUpL, ValUpR, ValDnL, ValDnR, EffUpL, EffUpR, EffDnL, EffDnR.
These are proved simultaneously by induction on the type precision derivation and by Löb-induction.

c : A A'

e : A' A”

^_d_σ M N : c
^_d_σ M A' A” N : c ∘e

We need to show that

\[ ({M}, {\upcast {A'} {A''} N}) \in
\simierel {d_\sigma} j {\simivrel {c \circ e} {}}. \]

The proof is by induction on the precision derivation $e$.
By monadic bind (Lemma <ref>), with $E_1 = \hole$ and
$E_2 = \upcast {A'} {A''} \hole$, it suffices to show

\[ ({V_1}, {\upcast {A'} {A''} V_2}) \in
\simierel {d_\sigma} k {\simivrel {c \circ e} {}},
\]

where $k \le j$ and $(V_1, V_2) \in \simivrel {c} {k}$.
We continue by cases on $e$.

* Case $e = \boolty$. We have $A = A' = A'' = \boolty$, and $c = \boolty$. Thus $c \circ e = \boolty$.

Examining the operational semantics, we see that

\[
({\upcast \boolty \boolty})({V_1}) \stepsin 1 {V_1}.
\]

Thus, by anti-reduction, it suffices to show

\[
({V_1}, {V_2}) \in
\simierel {d_\sigma} k {\simivrel {\boolty} {}}.
\]

This is true by assumption and Lemma <ref>.

* Case $e = e_i \to_{e_{\sigma}} e_o$. We have
$A'  = A_i'  \to_{\sigma_A' } A_o'$ and
$A'' = A_i'' \to_{\sigma_A''} A_o''$, and also
$e_i : A_i' \ltdyn A_i''$ and
$e_o : A_o' \ltdyn A_o''$.

By inversion, we see that $c = c_i \to_{c_\sigma} c_o$.

Thus, we have that
$c \circ e = (c_i \to_{c_\sigma} c_o) \circ (e_i \to_{e_{\sigma}} e_o) =
(c_i \circ e_i) \to_{c_\sigma \circ e_\sigma} (c_o \circ e_o)$.

We need to show that

\[
{\upcast {(A_i' \to_{\sigma_A'} A_o')} {(A_i'' \to_{\sigma_A''} A_o'')} V_2}
) \in \simierel {d_\sigma} k {\simivrel {(c_i \circ e_i) \to_{c_\sigma \circ e_\sigma} (c_o \circ e_o)} {}}.
\]

As both terms are values, it suffices by Lemma <ref>
to show they are related in ${\simivrel {(c_i \circ e_i) \to_{c_\sigma \circ e_\sigma} (c_o \circ e_o)} {k}}$.
To this end, let $k' \le k$ and $(V^l, V^r) \in \simivrel {c_i \circ e_i} {k'}$.
We need to show that

\[
({V_1}\, V^l,
(\upcast {(A_i' \to_{\sigma_A'} A_o')} {(A_i'' \to_{\sigma_A''} A_o'')} V_2)\, V^r) \in
\simierel {c_\sigma \circ e_\sigma} {k'} {\simivrel {c_o \circ e_o} {}}.
\]

By anti-reduction, it suffices to show that

\[
({V_1}\, V^l,
\upcast {A_o'} {A_o''} \upcast {\sigma_A'} {\sigma_A''} (V_2\, \dncast {A_i'} {A_i''} V^r) ) \in
\simierel {c_\sigma \circ e_\sigma} {k'} {\simivrel {c_o \circ e_o} {}}.
\]

By the induction hypothesis applied twice, it suffices to show

\[
({V_1}\, V^l,
(V_2\, \dncast {A_i'} {A_i''} V^r) ) \in
\simierel {c_\sigma} {k'} {\simivrel {c_o} {}}.
\]

Finally, it suffices by the soundness of the term precision congruence rule for
function application (Lemma <ref> to show
that $(V_1, V_2) \in \simivrel {c_i \to_{c_\sigma} c_o} {k'}$, and that

\[ (V^l, \dncast {A_i'} {A_i''} V^r) \in \simierel {d_\sigma} {k'} {\simivrel {c} {}}. \]

The former is true by our assumption on $V_1$ and $V_2$.
The latter follows by the induction hypothesis and our assumption on $V^l$ and $V^r$.

^⊢_d_σ c : A A'

^⊢_d_σ e : A' A”

^⊢_d_σ M N : c ∘e
^⊢_d_σ A A' M N : e

Let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} j$. We need to show that

\[
( {\upcast A {A'} M}[\gamma_1], {N}[\gamma_2] ) \in
\simierel {d_\sigma} j {\simivrel e {}}.
\]

By monadic bind (Lemma <ref>), with
$E_1 = \upcast {A} {A'} \hole$ and
$E_2 = \hole$, it suffices to show

\[
( {\upcast {A} {A'} V_1}, V_2 ) \in
\simierel {d_\sigma} j {\simivrel {e} {}},
\]

where $k \le j$ and $(V_1, V_2) \in \simivrel {c \circ e} {k}$.

We continue by cases on $c$.
The case $c = \boolty$ is similar to that in the previous lemma, so we skip to considering the case
$c = c_i \to_{c_\sigma} c_o$. By inversion, we see that $e = e_i \to_{e_\sigma} e_o$.

We have
$A  = A_i  \to_{\hat{\sigma} } A_o$ and
$A' = A_i' \to_{\hat{\sigma}'} A_o'$, and also
Thus, we have that $c \circ e = (c_i \circ e_i) \to_{c_\sigma \circ e_\sigma} (c_o \circ e_o)$.

We need to show that

\[
( {\upcast {(A_i  \to_{\hat{\sigma} } A_o)} {(A_i' \to_{\hat{\sigma}'} A_o')} M}[\gamma_1],
N[\gamma_2] ) \in
\simierel {d_\sigma} j {\simivrel {e_i \to_{e_\sigma} e_o} {}}.
\]

Similar to before, it suffices to show that these terms are related at $\simivrel {e_i \to_{e_\sigma} e_o} {k}$.
This is similar to proof of the previous lemma, and hence omitted.

^⊢_d_σ c : A A'

^⊢_d_σ e : A' A”

^⊢_d_σ M N : e
^⊢_d_σ A A' M N : c ∘e

This proof is dual to the proof of ValUpR-general (Lemma <ref>) and is hence omitted.

^⊢_d_σ c : A A'

^⊢_d_σ e : A' A”

^⊢_d_σ M N : c ∘e
^⊢_d_σ M A' A” N : c

This proof is dual to the proof of ValUpL-general (Lemma <ref>) and is hence omitted.

d_σ: σσ'

d_σ' : σ' σ”

^⊢_d_σ M N : c
M σ' σ” N : c

Let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} j$. We need to show that

\[
\expandTermPrecisionDef
{{\upcast {\sigma'} {\sigma''} N}}
{d_\sigma \circ d_\sigma'}{c}{j}.
\]

We prove this statement by Löb induction (Lemma <ref>).
That is, assume for all $k \le j$ and all
$(M', N') \in (\later \simierel {d_\sigma} {} {})_k ({\simivrel {c} {}})$,
we have

\[ (M', \upcast {\sigma'} {\sigma''} N')
\in (\later \simierel {d_\sigma \circ d_\sigma'} {} {})_{k} ({\simivrel {c} {}}).
\]

Let $(M, N) \in \simierel {d_\sigma} {j} {\simivrel {c} {}}$. We need to show

\[ (M, \upcast {\sigma'} {\sigma''} N)
\in \simierel {d_\sigma \circ d_\sigma'} {j} {\simivrel {c} {}}.
\]

We proceed by cases on $d_\sigma'$. The case $d_\sigma' = \dyn$ is immediate,
so consider $d_\sigma' = \texttt{inj}(d_c)$,
where $d_c : \sigma_c \ltdyn \sig \mid_{\textrm{supp}(\sigma_c)}$.
In this case, we know that $\sigma'' = \dyn$. Furthermore, we have

\[ d_\sigma \circ d_\sigma' = d_\sigma \circ (\texttt{inj} (d_c)) = \texttt{inj} (d_\sigma \circ d_c). \]

Thus, we need to show

\[
\expandTermPrecisionDef
{{\upcast {\sigma'} {\dyn} N}}
{\texttt{inj} (d_\sigma \circ d_c)}{c}{j}.
\]

By monadic bind (Lemma <ref>), it will suffice to consider the following cases:

* Let $k \le j$ and let $(V_1, V_2) \in \simivrel c k$. We need to show

\[
(V_1, {\upcast {\sigma'} {\dyn} V_2}) \in
\simierel {\texttt{inj} (d_\sigma \circ d_c)} k {\simivrel c {}}.
\]

By anti-reduction, it suffices to show that

\[
(V_1, V_2) \in
\simierel {\texttt{inj} (d_\sigma \circ d_c)} k {\simivrel c {}}.
\]

As $V_1$ and $V_2$ are values, it suffices by Lemma <ref> to
show that $(V_1, V_2) \in \simivrel c k$, which is true by assumption.

* Let $k \le j$ and $\effname @ c_\effname \leadsto d_\effname \in d_\sigma$
be an effect that is caught by ${\upcast {\sigma'} {\dyn} \hole}$.
Let $(V^l, V^r) \in (\later \simivrel {c_\effname} {})_k$, and
let $E^l \apart \effname$ and $E^r \apart \effname$ be evaluation contexts such that
$(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_\effname}{})_k
(\simierel{d_{\sigma}} {} {\simivrel c {}})$. We need to show that

\begin{align*}
( &E^l[\raiseOpwithM{\effname}{V^l}], \\
&\upcast {\sigma'} {\dyn}
E^r[\raiseOpwithM{\effname}{V^r}] ) \in
\simierel {\texttt{inj} (d_\sigma \circ d_c)} k {\simivrel c {}}.
\end{align*}

By anti-reduction, it suffices to show that

\begin{align*}
( &E^l[\raiseOpwithM{\effname}{V^l}], \\
{\dncast {d_\effname^r} {d_\effname^\dyn}
\raiseOpwithM
\effname
{\upcast {c_\effname^r} {c_\effname^\dyn} V^r}}
{\upcast {\sigma'} {\dyn} E^r[y]}
) \\
&\quad\quad \in
\simierel {\texttt{inj} (d_\sigma \circ d_c)} k {\simivrel c {}}.
\end{align*}

Let $V'^r$ be the term to which $\upcast {c_\effname^r} {c_\effname^\dyn} V^r$ steps.
By anti-reduction, it suffices to show

\begin{align*}
( &E^l[\raiseOpwithM{\effname}{V^l}], \\
{\dncast {d_\effname^r} {d_\effname^\dyn} \raiseOpwithM{\effname}{V'^r}}
{\upcast {\sigma'} {\dyn} E^r[y]}
) \\
&\quad\quad \in
\simierel {\texttt{inj} (d_\sigma \circ d_c)} k {\simivrel c {}}.
\end{align*}

As neither term steps, it suffices to show they are related in
$\simirrel {\texttt{inj} (d_\sigma \circ d_c)} k {\simivrel c {}}.$.
To this end, we need to show (1) $(V^l, V'^r) \in (\later \simivrel {c_\effname \circ c'_\effname} {})_{k}$,
and (2) given $k' \le k$ and $(V_1, V_2) \in (\later \simivrel {d_\effname \circ d'_\effname} {})_{k'}$, we

\begin{align*}
( &E^l[V_1], \\
{\dncast {d_\effname^r} {d_\effname^\dyn} V_2}
{\upcast {\sigma'} {\dyn} E^r[y]}
) \\
&\quad\quad \in
(\later \simierel {\inj I {d_\sigma \circ d_c}} {} {})_{k'} ({\simivrel c {}}).
\end{align*}

To show (1), it suffices by forward reduction to show that
$(V^l, \upcast {c_\effname^r} {c_\effname^\dyn} V^r) \in (\later \simivrel {c_\effname \circ c'_\effname} {})_{k}$.
This follows inductively from ValUpR (which we are proving simultaneously and can
therefore apply at smaller types), and our assumption on $V^l$ and $V^r$.

To show (2), let $V_2'$ be the value to which
$\dncast {d_\effname^r} {d_\effname^\dyn} V_2$ steps.
It suffices by anti-reduction to show

\begin{align*}
( &E^l[V_1],
{\upcast {\sigma'} {\dyn} E^r[V_2']}
) \\
&\quad\quad \in
(\later \simierel {\inj I {d_\sigma \circ d_c}} {} {})_{k'} ({\simivrel c {}}).
\end{align*}

By the Löb induction hypothesis, it suffices to show that

\begin{align*}
( &E^l[V_1], {E^r[V_2']} ) \\
&\quad\quad \in
(\later \simierel {d_\sigma} {} {})_{k'} ({\simivrel c {}}).
\end{align*}

By our assumption on $E^l$ and $E^r$, it suffices to show that
$(V_1, V_2') \in (\later \simivrel {d_\effname} {})_{k'}$.
By forward reduction, it suffices to show that

\[
(V_1, \dncast {d_\effname^r} {d_\effname^\dyn} V_2) \in
(\later \simierel {d_\sigma} {} {})_{k'} (\simivrel {d_\effname} {}).
\]

Now inductively by ValDnR, it suffices to show
$(V_1, V_2) \in (\later \simivrel {d_\effname \circ d'_\effname} {})_{k'}$,
which is our assumption.

The case where $d_\sigma'$ is a concrete effect precision derivation is similar to the above.

d_σ: σσ'

d_σ' : σ' σ”

^⊢_d_σ∘d_σ' M N : c
^⊢_d_σ' σσ' M N : c

This is proved similarly to the above.

d_σ: σσ'

d_σ' : σ' σ”

^⊢_d_σ' M N : c
^⊢_d_σ∘d_σ' σ σ' M N : c

We prove this by Löb induction (Lemma <ref>).
That is, assume for all $k \le j$ and all
$(M', N') \in (\later \simierel {d_\sigma'} {} {})_k ({\simivrel {c} {}})$,
we have

\[ (\dncast {\sigma} {\sigma'} M', N')
\in (\later \simierel {d_\sigma \circ d_\sigma'} {} {})_{k} ({\simivrel {c} {}}).
\]

Let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} j$, and let
$(M, N) \in \simierel {d_\sigma'} {j} {\simivrel {c} {}}$. We need to show

\[ (\dncast {\sigma} {\sigma'} M, N)
\in \simierel {d_\sigma \circ d_\sigma'} {j} {\simivrel {c} {}}.
\]

By monadic bind (Lemma <ref>) and the fact that effect casts are the
identity on values, it will suffice to show the following:

Let $k \le j$ and $\effname @ c_\effname \leadsto d_\effname \in d_\sigma'$
be an effect that is caught by ${\dncast {\sigma} {\sigma'} \hole}$.
Let $(V^l, V^r) \in (\later \simivrel {c_\effname} {})_k$, and
let $E^l \apart \effname$ and $E^r \apart \effname$ be evaluation contexts such that
$(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_\effname}{})_k
(\simierel{d_\sigma'} {} {\simivrel c {}})$. We need to show that

\begin{align*}
& \dncast {\sigma} {\sigma'}
E^l[\raiseOpwithM{\effname}{V^l}], \\
& E^r[\raiseOpwithM{\effname}{V^r}]N
\\ & \quad \quad \in \simierel {d_\sigma \circ d_\sigma'} {j} {\simivrel {c} {}}.
\end{align*}

Note that if $\effname \notin \sigma$, then the left hand side steps to $\err$,
in which case we are finished by ErrBot (Lemma <ref>).
Otherwise, the proof proceeds alalogously to EffUpR (Lemma <ref>),
with upcasts and downcasts interchanged.

d_σ: σσ'

d_σ' : σ' σ”

^⊢_d_σ∘d_σ' M N : c
^⊢_d_σ M σ' σ” N : c

We prove this statement by Löb induction (Lemma <ref>).
That is, assume for all $k \le j$ and all
$(M', N') \in (\later \simierel {d_\sigma \circ d_\sigma'} {} {})_k ({\simivrel {c} {}})$,
we have

\[ (M', \dncast {\sigma'} {\sigma''} N')
\in (\later \simierel {d_\sigma} {} {})_{k} ({\simivrel {c} {}}).
\]

Let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma^\ltdyn} j$, and let
$(M, N) \in \simierel {d_\sigma \circ d_\sigma'} {j} {\simivrel {c} {}}$. We need to show

\[ (M, \dncast {\sigma'} {\sigma''} N)
\in \simierel {d_\sigma} {j} {\simivrel {c} {}}.
\]

By monadic bind (Lemma <ref>) and the fact that effect casts are the
identity on values, it will suffice to show the following:

Let $k \le j$ and $\effname @ c_\effname \leadsto d_\effname \in d_\sigma \circ d_\sigma'$
be an effect that is caught by ${\dncast {\sigma'} {\sigma''} \hole}$.
Let $(V^l, V^r) \in (\later \simivrel {c_\effname} {})_k$, and
let $E^l \apart \effname$ and $E^r \apart \effname$ be evaluation contexts such that
$(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel{d_\effname}{})_k
(\simierel{d_{\sigma} \circ d_\sigma'} {} {\simivrel c {}})$. We need to show that

\begin{align*}
( &E^l[\raiseOpwithM{\effname}{V^l}], \\
&\dncast {\sigma'} {\sigma''}
E^r[\raiseOpwithM{\effname}{V^r}] ) \in
\simierel {d_\sigma} k {\simivrel c {}}.
\end{align*}

First note that by Lemma <ref>, there exist
$c_1$, $c_2$, $d_1$, and $d_2$ such that
$c_\effname = c_1 \circ c_2$ and $d_\effname = d_1 \circ d_2$ and
$\effname @ c_1 \leadsto d_1 \in d_\sigma$ and $\effname @ c_2 \leadsto d_2 \in d_\sigma'$.
In particular, this that $\effname \in \sigma'$, so the downcast from $\sigma''$ to $\sigma'$ does not fail.
Let $c^L = c_1^l (= c_\effname^l)$,
$c^M = c_1^r = c_2^l$,
and $c^R = c_2^r (= c_\effname^r)$, and likewise define $d^L, d^M$ and $d^R$.

By anti-reduction, it suffices to show that

\begin{align*}
( &E^l[\raiseOpwithM{\effname}{V^l}], \\
{\upcast {d^M} {d^R}
\raiseOpwithM
\effname
{\dncast {c^M} {c^R} V^r}}
{\dncast {\sigma'} {\sigma''} E^r[y]}
) \\
&\quad\quad \in
\simierel {d_\sigma} k {\simivrel c {}}.
\end{align*}

Let $V'^r$ be the term to which $\dncast {c^M} {c^R} V^r$ steps.
By anti-reduction, it suffices to show

\begin{align*}
( &E^l[\raiseOpwithM\effname{V^l}], \\
{\upcast {d^M} {d^R}
\raiseOpwithM
\effname
{\dncast {\sigma'} {\sigma''} E^r[y]}
) \\
&\quad\quad \in
\simierel {d_\sigma} k {\simivrel c {}}.
\end{align*}

As neither term steps, it suffices to show they are related in
$\simirrel {d_\sigma} k {\simivrel c {}}$.
To this end, we need to show (1) $(V^l, V'^r) \in (\later \simivrel {c_1} {})_{k}$,
and (2) given $k' \le k$ and $(V_1, V_2) \in (\later \simivrel {d_1} {})_{k'}$, we

\begin{align*}
( &E^l[V_1], \\
{\upcast {d^M} {d^R} V_2}
{\dncast {\sigma'} {\sigma''} E^r[y]}
) \\
&\quad\quad \in
(\later \simierel {d_\sigma} {} {})_{k'} ({\simivrel c {}}).
\end{align*}

(1) follows from forward reduction and the inductive hypothesis for value types.
To show (2), let $V_2'$ be the value to which
$\upcast {d^M} {d^R} V_2$ steps.
It suffices by anti-reduction to show

\begin{align*}
( &E^l[V_1],
{\upcast {\sigma'} {\sigma''} E^r[V_2']}
) \\
&\quad\quad \in
(\later \simierel {d_\sigma} {} {})_{k'} ({\simivrel c {}}).
\end{align*}

By the Löb induction hypothesis, it suffices to show that

\begin{align*}
( &E^l[V_1], {E^r[V_2']} ) \\
&\quad\quad \in
(\later \simierel {d_\sigma \circ d_\sigma'} {} {})_{k'} ({\simivrel c {}}).
\end{align*}

By our assumption on $E^l$ and $E^r$, it suffices to show that
$(V_1, V_2') \in (\later \simivrel {d_\effname} {})_{k'}$.
By forward reduction, it suffices to show that

\[
(V_1, \upcast {d^M} {d^R} V_2) \in
(\later \simierel {d_\sigma} {} {})_{k'} (\simivrel {d_\effname} {}).
\]

Now inductively by ValUpR, it suffices to show
$(V_1, V_2) \in (\later \simivrel {d_1} {})_{k'}$,
which is our assumption.

The case where $d_\sigma'$ is a concrete effect precision derivation is similar to the above.

*[]A B M ≡M x A B x

We show one direction of the equivalence; the other is symmetric.
Let $j$ be arbitrary and let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show

\[
(\upcast A B M)[\gamma_1], \,
(\letXbeboundtoYinZ M x \upcast A B x)[\gamma_2]
) \in \simierel {\sigma} {j} {\simivrel {B} {}}.
\]

By Monadic Bind (Lemma <ref>) and reflexivity, it will suffice to
show that for all $k \le j$ let $(V_1, V_2) \in \simivrel {A} {k}$, we have

\[
(\upcast A B V_1), \,
(\letXbeboundtoYinZ {V_2} x \upcast A B x)
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

By anti-reduction, it suffices to show

\[
(\upcast A B V_1), \,
(\upcast A B V_2)
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

By congruence, it suffices to show

\[
V_1, \, V_2
) \in \simierel {\sigma} {k} {\simivrel {B} {}}.
\]

This follows from our assumption on $V_1$ and $V_2$.

*[]A B M ≡M x A B x

Dual to the above.

let $A \ltdyn B$ and $\sigma \ltdyn \sigma'$, and let $c : A \ltdyn B$
and $d_\sigma : \sigma \ltdyn \sigma'$.
Let $\sg^\ltdyn \vdash_{\sigma} M \ltdyn N : A$.
The following hold:

* $\sg^\ltdyn \vDash_{\sigma} \dncast{A}{B} \upcast{A}{B} M \ltdyn N : A$

* $\sg^\ltdyn \vDash_{\sigma} \dncast{\sigma}{\sigma'} \upcast{\sigma}{\sigma'} M \ltdyn N : A$

We prove stronger, “pointwise" version of the above statemenets. Namely, we assume
$(M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$,
and show, for example, that
$(\dncast{A}{B} \upcast{A}{B} M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$.

The proof is by simultaneous induction on the derivations $c$ and $d_\sigma$.

* Let $(\gamma_1, \gamma_2) \in \simigrel {A} {j}$.
Suppose $(M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$.
We need to show

\[ (\dncast{A}{B} \upcast{A}{B} M, N)
\in \simierel {\sigma} {j} {\simivrel {A} {}}. \]

By monadic bind (Lemma <ref>), it suffices to show that

\[ (\dncast{A}{B} \upcast{A}{B} V_1, V_2) \in \simierel {\sigma} {k} {\simivrel {A} {}}, \]

where $k \le j$ and $(V_1, V_2) \in \simivrel {A} {k}$.

We proceed by induction on the precision derivation $c$. If $c = \boolty$, then we need to show

\[ (\dncast{\boolty}{\boolty} \upcast{\boolty}{\boolty} V_1, V_2) \in
\simierel {\sigma} {k} {\simivrel {\boolty} {}}. \]

According to the operational semantics, we have that

\[ \dncast{\boolty}{\boolty} \upcast{\boolty}{\boolty} V_1 \stepsin 2 V_1. \]

So by anti-reduction (Lemma <ref>), it suffices to show that
$(V_1, V_2) \in \simierel {\sigma} {k} {\simivrel {\boolty} {}}$, which follows from our assumption.

If $c = c_i \to_{c_\sigma} c_o$, then $A = A_i \to_{\sigma_A} A_o$ and $B = B_i \to_{\sigma_B} B_o$.
We need to show

\begin{align*} (\dncast{(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)}
&\upcast{(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} V_1,
V_2) \\
&\quad \quad \in \simierel {\sigma} {k} {\simivrel {A_i \to_{\sigma_A} A_o} {}}.
\end{align*}

As both of these are values, it suffices to show that they are related in
$\simivrel {A_i \to_{\sigma_A} A_o} {}$. To this end, let $k' \le k$ and let
$(V^l, V^r) \in \simivrel {A_i} {k'}$. We need to show that

\begin{align*} (
&(\dncast{(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)}
\upcast{(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} V_1)\, V^l, \\
&V_2\, V^r)\\
&\quad \quad \in \simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\end{align*}

The former term steps, so by anti-reduction, it suffices to show that

\begin{align*}
&\dncast{A_o} {B_o} &\dncast {\sigma_A} {\sigma_B}
((\upcast{(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} V_1)\, \upcast {A_i} {B_i} V^l),
&V_2\, V^r
&\quad \quad \in \simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\end{align*}

Let $V'^l$ be the value to which $\upcast {A_i} {B_i} V^l$ steps.
By anti-reduction, it suffices to show that

\begin{align*}
&\dncast{A_o} {B_o} \dncast {\sigma_A} {\sigma_B} \\
&\quad\quad  (\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} \\
&\quad\quad\quad\quad (V_1\, \dncast {A_i} {B_i} V'^l)), \\
&V_2\, V^r
&\quad \quad \in \simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\end{align*}

We will appeal to transitivity (Lemma <ref>).
We continue by cases on $\sim$. First assume $\sim$ is $<$.
Let $V'^r$ be the value to which $\upcast {A_i} {B_i} V^r$ steps. If we show (1)

\begin{align*}
&\dncast{A_o} {B_o} \dncast {\sigma_A} {\sigma_B} \\
&\quad\quad  (\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} \\
&\quad\quad\quad\quad (V_1\, \dncast {A_i} {B_i} V'^l)), \\
&\dncast{A_o} {B_o} \upcast {A_o} {B_o} \\
&\quad\quad  (\dncast {\sigma_A} {\sigma_B} \upcast {\sigma_A} {\sigma_B} \\
&\quad\quad\quad\quad (V_2\, \dncast {A_i} {B_i} V'^r))
&\quad \quad \in \simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\end{align*}

and (2)

\begin{align*}
&\dncast{A_o} {B_o} \upcast {A_o} {B_o} \\
&\quad\quad  (\dncast {\sigma_A} {\sigma_B} \upcast {\sigma_A} {\sigma_B} \\
&\quad\quad\quad\quad (V_2\, \dncast {A_i} {B_i} V'^r)), \\
&V_2\, V^r
&\quad \quad \in \simierel {\sigma_A} {\omega} {\simivrel {A_o} {}},
\end{align*}

then we will be finished by transitivity.

To show (1), first note that by monotonicity of casts (Lemma <ref>),
it suffices to show that

\begin{align*}
&\dncast {\sigma_A} {\sigma_B} \\
&\quad\quad  (\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} \\
&\quad\quad\quad\quad (V_1\, \dncast {A_i} {B_i} V'^l)), \\
&\upcast {A_o} {B_o} \\
&\quad\quad  (\dncast {\sigma_A} {\sigma_B} \upcast {\sigma_A} {\sigma_B} \\
&\quad\quad\quad\quad (V_2\, \dncast {A_i} {B_i} V'^r))
&\quad \quad \in \simierel {\sigma_A} {k'} {\simivrel {B_o} {}}.
\end{align*}

Then by commutativity of casts (Corollary <ref>),
it suffices to show

\begin{align*}
&\upcast {\sigma_A} {\sigma_B} (V_1\, \dncast {A_i} {B_i} V'^l), \\
&\upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V'^r)
&\quad \quad \in \simierel {\sigma_B} {k'} {\simivrel {A_o} {}}.
\end{align*}

By monotonicity of casts again, it suffices to show

\begin{align*}
&(V_1\, \dncast {A_i} {B_i} V'^l), \\
&(V_2\, \dncast {A_i} {B_i} V'^r)
&\quad \quad \in \simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\end{align*}

By soundness of the precision rule for function application, it suffices to
show that $(V_1, V_2) \in \simivrel {(A_i \to_{\sigma_A} A_o)} {k}$ and that
$(\dncast {A_i} {B_i} V'^l, \dncast {A_i} {B_i} V'^r) \in \simierel {\sigma_A} {k} {\simivrel {A_i} {}}$.
The former holds by assumption, and to show the latter, it suffices by forward reduction to show
$(\dncast {A_i} {B_i} \upcast {A_i} {B_i} V^l, \dncast {A_i} {B_i} \upcast {A_i} {B_i} V^r) \in
\simierel {\sigma_A} {k} {\simivrel {A_i} {}}$. This follows from the inductive hypothesis and
assumption on $V^l$ and $V^r$.

To show (2), it suffices by the inductive hypothesis applied twice to show

\begin{align*}
&(V_2\, \dncast {A_i} {B_i} V'^r)),
V_2\, V^r
&\quad \quad \in \simierel {\sigma_A} {\omega} {\simivrel {A_o} {}},
\end{align*}

By forward reduction, it suffices to show

\begin{align*}
&(V_2\, \dncast {A_i} {B_i} V'^r)),
V_2\, V^r
&\quad \quad \in \simierel {\sigma_A} {\omega} {\simivrel {A_o} {}},
\end{align*}

By soundness of function application, it suffices to show
that $V_2$ is related to itself at $\simivrel {(A_i \to_{\sigma_A} A_o)} {\omega}$
and that $(\dncast {A_i} {B_i} V'^r, V^r) \in \simierel {\sigma_A} {\omega} {\simivrel {A_i} {}}$.
The former holds by reflexivity (Corollary <ref>), and to show the
latter it suffices by forward reduction to show that

\[
(\dncast {A_i} {B_i} \upcast {A_i} {B_i} V^r, V^r) \in
\simierel {\sigma_A} {\omega} {\simivrel {A_i} {}},
\]

which follows by the inductive hypothesis and reflexivity.

The case when $\sim$ is $<$ is analogous.

* Let $(\gamma_1, \gamma_2) \in \simigrel {A} {j}$.
We use Löb induction. We assume that for all $k \le j$ and all related terms
$(M', N') \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {})$, we have

\[ (\dncast{\sigma}{\sigma'} \upcast{\sigma}{\sigma'} M', N')
\in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {}). \]

Let $(M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$. We need to show that

\[ (\dncast{\sigma}{\sigma'} \upcast{\sigma}{\sigma'} M, N)
\in \simierel {\sigma} {j} {\simivrel {A} {}}. \]

By monadic bind (Lemma <ref>), it suffices to consdier
the following cases:

* Let $k \le j$ and $(V_1, V_2) \in \simivrel {A} {k}$. We need to show

\begin{align*}
&(\dncast{\sigma}{\sigma'} \upcast{\sigma}{\sigma'} V_1, V_2) \in
\simierel {\sigma} {k} {\simivrel {A} {}}
\end{align*}

This follows by anti-reduction and assumption.

* Let $k \le j$ and let
$\effname @ C \leadsto D \in \sigma$.
Let $C'$ and $D'$ be the types such that
$\effname @ C' \leadsto D' \in \sigma'$.
Let $(V^l, V^r) \in (\later \simivrel {C} {})_{k}$
and let $E^l\apart \effname$ and $E^r \apart \effname$ be such that

\[
(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel {D})_{k} (\simierel {\sigma} {} {\simivrel {A} {}}).
\]

We need to show that

\begin{align*}
&\dncast{\sigma}{\sigma'} \upcast{\sigma}{\sigma'} E^l[\raiseOpwithM{\effname}{V^l}],
\\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

The first term steps, so by anti-reduction it suffices to show

\begin{align*}
&\dncast{\sigma}{\sigma'} (
\letXbeboundtoYinZ
{\dncast {D} {D'} \raiseOpwithM{\effname}{\upcast {C} {C'} V^l}}
{\upcast {\sigma} {\sigma'} E^l[x]}
), \\
\\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

Let $V'^l$ be the value to which $\upcast {C} {C'} V^l$ steps.
By anti-reduction, it suffices to show

\begin{align*}
{\upcast {D} {D'} \raiseOpwithM{\effname}{\dncast {C} {C'} V'^l}}
{\dncast {\sigma} {\sigma'}
\letXbeboundtoYinZ
{\dncast {D} {D'} y}
{\upcast {\sigma} {\sigma'} E^l[x]}
}, \\
\\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

Let $y'$ be the value to which $\dncast {D} {D'} y$ steps.
Let $V''^l$ be the value to which $\dncast {C} {C'} V'^l$ steps.

By anti-reduction, it suffices to show

\begin{align*}
{\upcast {D} {D'} \raiseOpwithM{\effname}{V''^l}}
{\dncast {\sigma} {\sigma'}
{\upcast {\sigma} {\sigma'} E^l[y']}
}, \\
\\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

Neither term steps, so it suffices to show they are related in
$\simirrel {\sigma} {k} {\simivrel {A} {}}$. To this end, we first
show that $(V''^l, V^r) \in (\later \simivrel {C} {})_{k}$.
By forward reduction, it suffices to show that
$(\dncast {C} {C'} \upcast {C} {C'} V^l, V^r) \in (\later \simivrel {C} {})_{k}$.
This follows from the inductive hypothesis for value types and our assumption on
$V^l$ and $V^r$.

We now show that, given $k' \le k$ and values
$(V_1, V_2) \in (\later \simivrel {D} {})_{k'}$, we have

\begin{align*}
{\upcast {D} {D'} V_1}
{\dncast {\sigma} {\sigma'}
{\upcast {\sigma} {\sigma'} E^l[y']}
}, \\
\\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {}).
\end{align*}

Let $V_1'$ be the value to which $\upcast {D} {D'} V_1$ steps.
By anti-reduction, it will suffice to show

\begin{align*}
{\dncast {\sigma} {\sigma'}
{\upcast {\sigma} {\sigma'} E^l[y']}
}, \\
\\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {}).
\end{align*}

By forward reduction, it will suffice to show

\begin{align*}
{\dncast {\sigma} {\sigma'}
{\upcast {\sigma} {\sigma'} E^l[\dncast {D} {D'} y]}
}, \\
\\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {}).
\end{align*}

By anti-reduction, it will suffice to show

\begin{align*}
&{\dncast {\sigma} {\sigma'} {\upcast {\sigma} {\sigma'} E^l[\dncast {D} {D'} V_1']}},
\\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {}).
\end{align*}

By the Löb induction hypothesis, it suffices to show that

\begin{align*}
&E^l[\dncast {D} {D'} V_1'], E^r[V_2]
\\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {}).
\end{align*}

By forward reduction, it suffices to show

\begin{align*}
&E^l[\dncast {D} {D'} \upcast {D} {D'} V_1], E^r[V_2]
\\ & \quad \quad \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {}).
\end{align*}

By the induction hypothesis for value types, it suffices to show

\[
( E^l[V_1], E^r[V_2] ) \in (\later \simierel {\sigma} {} {})_{k} (\simivrel {A} {}).
\]

This follows by our assumption on $E^l$ and $E^r$.

Let $c : A \ltdyn B$ and $c' : A' \ltdyn B'$ where $A \subty A'$ and $B \subty B'$.
Let $d_\sigma : \sigma_1 \ltdyn \sigma_2$ and $d_\sigma' : \sigma_1' \ltdyn \sigma_2'$ where
$\sigma_1 \subty \sigma_1'$ and $\sigma_2 \subty \sigma_2'$.
Suppose $M \equiv N$.
The following hold:

^_d_τ M N : A
^_d_τ A B M A' B' N : B'

^_d_τ M N : B
^_d_τ A' B' M A B N : A'

^_σ_1 M N : d
^_σ_2' σ_1 σ_2 M σ_1' σ_2' N : d

^_σ_2 M N : d
^_σ_1' σ_1' σ_2' M σ_1 σ_2 N : d

By simultaneous induction on the derivation $c' : A' \ltdyn B'$ and $d_\sigma' : \sigma_1' \ltdyn \sigma_2'$.

* We need to show

\[
( \upcast {A} {B} M, \upcast {A'} {B'} N ) \in
\simierel {d_\sigma} {j} {\simivrel {B'} {}}.
\]

By monadic bind (Lemma <ref>), with
$E_1 = \upcast {A} {B} \hole$ and $E_2 = \upcast {A'} {B'} \hole$, it suffices to show the following.

Let $k \le j$ and let $(V_1, V_2) \in \simivrel {A'} k$.
We need to show

\[ (\upcast {A} {B} V_1, \upcast {A'} {B'} V_2) \in
\simierel {d_\sigma} {k} {\simivrel {B'} {}}. \]

We continue by cases on $c'$.

Case $c' = \boolty$. Then by inversion on the rules for subtyping of precision derivations,
we have $c = \boolty$.

We need to show

\[ (\upcast \boolty \boolty V_1, \upcast \boolty \boolty V_2) \in
\simierel {d_\sigma} {k} {\simivrel {\boolty} {}}
\]

This follows by anti-reduction and our assumption on $V_1$ and $V_2$.

Case $c' = c_i' \to_{c_\sigma'} c_o' : A_i' \to_{\sigma_A'} A_o' \ltdyn B_i' \to_{\sigma_B'} B_o'$.

By inversion on the rules for subtyping for precision derivations, we have that
$c = c_i \to_{c_\sigma} c_o$, where
$c_i' \subty c_i$, and $c_\sigma \subty c_\sigma'$, and $c_o \subty c_o'$.

Our assumption then becomes $(V_1, V_2) \in \simivrel {A_i' \to_{\sigma_A'} A_o'} k$.
We need to show

\[
( \upcast {A_i \to_{\sigma_A} A_o} {B_i \to_{\sigma_B} B_o} V_1,
\upcast {A_i' \to_{\sigma_A'} A_o'} {B_i' \to_{\sigma_B'} B_o'} V_2 ) \in
\simierel {d_\sigma} {k} {\simivrel {B_i' \to_{\sigma_B'} B_o'} {}}.
\]

Since both terms are values, it suffices to show they are related in
$\simivrel {B_i' \to_{\sigma_B'} B_o'} {k}$.
Let $k' \le k$ and let $(V^l, V^r) \in \simivrel {B_i'} {k'}$.
We need to show

\begin{align*}
( &(\upcast {A_i \to_{\sigma_A} A_o} {B_i \to_{\sigma_B} B_o} V_1)\, V^l, \\
&(\upcast {A_i' \to_{\sigma_A'} A_o'} {B_i' \to_{\sigma_B'} B_o'} V_2)\, V^r ) \\
& \quad \quad \in \simierel {\sigma_B'} {k'} {\simivrel {B_o'} {}}.
\end{align*}

By anti-reduction, it suffices to show

\begin{align*}
( &\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} (V_1\, \dncast {A_i} {B_i} V^l), \\
&\upcast {A_o'} {B_o'} \upcast {\sigma_A'} {\sigma_B'} (V_2\, \dncast {A_i'} {B_i'} V^r) ) \\
& \quad \quad \in \simierel {\sigma_B'} {k'} {\simivrel {B_o'} {}}.
\end{align*}

By the induction hypothesis applied twice, it suffices to show

\begin{align*}
( &(V_1\, \dncast {A_i} {B_i} V^l),
(V_2\, \dncast {A_i'} {B_i'} V^r) ) \\
& \quad \quad \in \simierel {\sigma_A'} {k'} {\simivrel {A_o'} {}}.
\end{align*}

By soundness of the term precision congruence rule for function application (Lemma <ref>),
it suffices to show that $(V_1, V_2) \in \simivrel {A_i' \to_{\sigma_A'} A_o'} {k'}$,
and that

\[
(\dncast {A_i} {B_i} V^l, \dncast {A_i'} {B_i'} V^r) \in \simierel {d_\sigma} {k'} {\simivrel {A_i'} {}}.
\]

The former holds by assumption.
To show the latter, it suffices by the admissible direction of gradual subtyping rule ValDnSub (item (2)
in Lemma <ref>), whose proof does not depend on the present lemma,
to show that $(V^l, V^r) \in \simivrel {B_i'} {k'}$. This is true by assumption.

* Similar to the above.

* We need to show

\[ (\upcast {\sigma_1} {\sigma_2} M, \upcast {\sigma_1'} {\sigma_2'} N) \in
\simierel {\sigma_2'} {j} {\simivrel {c} {}}. \]

We use Löb induction. That is, we assume as our induction hypothesis that

\[
\upcast {\sigma_1} {\sigma_2} M',
\upcast {\sigma_1'} {\sigma_2'} N'
) \in \later (\simierel {\sigma_2'} {})_{j} {(\simivrel {c} {})},
\]

for all $(M', N') \in (\later \simierel {\sigma_1'} {} {})_{j} (\simivrel {c} {})$,
and we show that under this assumption, we have

\[
\upcast {\sigma_1} {\sigma_2} M,
\upcast {\sigma_1'} {\sigma_2'} N
) \in \simierel {\sigma_2'} {j} {\simivrel {c} {}}
\]

for all $(M, N) \in \simierel {\sigma_1'} {j} {\simivrel {c} {}}$.

Using Monadic Bind (Lemma <ref>), we have the following cases:

* Let $k \le j$ and $(V_1, V_2) \in \simivrel c k$.
We need to show

\[ (\upcast {\sigma_1} {\sigma_2} V_1, \upcast {\sigma_1'} {\sigma_2'} V_2) \in
\simierel {\sigma_2'} {k} {\simivrel {c} {}}. \]

This follows by anti-reduction and our assumption on $V_1$ and $V_2$.

* Let $\effname @ c_i \leadsto d_i \in \sigma_1$ be an effect caught by
$\upcast {\sigma_1'} {\sigma_2'} \hole$.
Let $(V^l, V^r) \in (\later \simivrel {c_i^l} {})_k$, and let
$(E^l, E^r) \in (\later \simikrel {d_i^l} {})_k (\simierel {\sigma_1'} {} {\simivrel {c} {}})$.
We need to show

\begin{align*}
& \upcast {\sigma_1} {\sigma_2} E^l[\raiseOpwithM{\effname}{V^l}],
\upcast {\sigma_1'} {\sigma_2'} E^r[\raiseOpwithM{\effname}{V^r}]
) \\ & \quad \quad \in \simierel {\sigma_2'} {k} {\simivrel {c} {}}.
\end{align*}

We continue by cases on subtyping of effect precision derivations.
We show only the case $d_\sigma'$ is a concrete effect precision set $d_c'$;
the other cases follow immediately or reduce to this one.

By inversion, we have $d_\sigma$ is also a concrete effect precision set $d_c$ where
$\dom(d_c) \subseteq \dom(d'_c)$ and
for all $\effarr \effname c d \in d_c$,
$\effarr \effname {c'} {d'} \in d'_c$ and  $c \subty c'$ and $d' \subty d$.
By anti-reduction, it suffices to show

\begin{align*}
& \letXbeboundtoYinZ
{\dncast {d_i^l} {d_i^r} \raiseOpwithM{\effname}{\upcast {c_i^l} {c_i^r} V^l}}
{x} {\upcast {\sigma_1} {\sigma_2} E^l[x]}, \\
& \letXbeboundtoYinZ
{\dncast {d_i'^l} {d_i'^r} \raiseOpwithM{\effname}{\upcast {c_i'^l} {c_i'^r} V^r}}
{x} {\upcast {\sigma_1'} {\sigma_2'} E^r[x]}
) \\ & \quad \quad \in (\later \simierel {\sigma_2'})_{k} ({\simivrel {c} {}}),
\end{align*}

By congruence for Let, it suffices to show (1)

\begin{align*}
& {\dncast {d_i^l} {d_i^r} \raiseOpwithM{\effname}{\upcast {c_i^l} {c_i^r} V^l}}, \\
& {\dncast {d_i'^l} {d_i'^r} \raiseOpwithM{\effname}{\upcast {c_i'^l} {c_i'^r} V^r}}
) \\ & \quad \quad \in (\later \simierel {\sigma_2'})_{k} ({\simivrel {c} {}}),
\end{align*}

and (2) for $(V_1, V_2) \in \later (\simivrel {d_i} {})_k$ we have

\begin{align*}
& {\upcast {\sigma_1} {\sigma_2} E^l[V_1]}, \\
& {\upcast {\sigma_1'} {\sigma_2'} E^r[V_2]}
) \\ & \quad \quad \in (\later \simierel {\sigma_2'})_{k} ({\simivrel {c} {}}),
\end{align*}

To show (1), first note that by the induction hypothesis for value types,

\[
\raiseOpwithM{\effname}{\upcast {c_i^l} {c_i^r} V^l},
\raiseOpwithM{\effname}{\upcast {c_i'^l} {c_i'^r} V^r}
) \in \simierel {\sigma_2'} {k} {\simivrel {c_i'} {}},
\]

and by the induction hypothesis for value types again, (1) follows.
To show (2), note that $E^l[x^l]$ and $E^r[x^r]$ are related by
assumption on $E^l$ and $E^r$. So we may apply the Löb induction hypothesis
to reach the desired conclusion.

* We again use Löb induction and monadic bind. In the related raises case of the bind lemma,
we let
$\effname @ c_i \leadsto d_i \in \sigma_2$ be an effect caught by
$\upcast {\sigma_1'} {\sigma_2'} \hole$. We let
$(V^l, V^r) \in (\later \simivrel {c_i^l} {})_k$, and let
$(E^l, E^r) \in (\later \simikrel {d_i^l} {})_k (\simierel {\sigma_1'} {} {\simivrel {c} {}})$.

We need to show

\begin{align*}
& \upcast {\sigma_1} {\sigma_2} E^l[\raiseOpwithM{\effname}{V^l}],
\upcast {\sigma_1'} {\sigma_2'} E^r[\raiseOpwithM{\effname}{V^r}]
) \\ & \quad \quad \in \simierel {\sigma_2'} {k} {\simivrel {c} {}}.
\end{align*}

If $\effname \notin \sigma_1$, then both sides step to $\err$. Since $\err$ is
related to itself by ErrBot (Lemma <ref>), we are finished by anti-reduction.

Otherwise, the proof proceeds analogously to that of the previous case, with
upcasts and downcasts interchanged.

Let $E$ be an evaluation context such that
(1) for all $\sigma$, $\hastyGDRhoMT{\Gamma}{\holeRhoT{\sigma}{A}}{\sigma}{E}{B}$,
and such that (2) $E \apart \effname$ for all $\effname \in \Sigma$.
Furthermore, suppose that (3) for all values $V$, there exists a value $V'$ such that $E[V] \stepsin * V'$.

Let $\sg^\ltdyn \vDash_{\sigma_2} M \equiv N : A$.

Then $\sg^\ltdyn \vDash_{\sigma_1} E[\dncast {\sigma_1}{\sigma_2} M] \equiv
\dncast {\sigma_1} {\sigma_2} E[N] : B$,
and likewise for upcasts.

We show the statement for downcasts only; the proof for upcasts is similar.
Additionally, we show only one of the directions of the equivalence; the other is symmetric.

We need to show

\[ ( E[\dncast {\sigma_1}{\sigma_2} M], \dncast {\sigma_1} {\sigma_2} E[N] ) \in
\simierel {\sigma_1} {j} {\simivrel {B} {}}. \]

We apply monadic bind (Lemma <ref>) with $E_1 = E[\dncast {\sigma_1}{\sigma_2} \hole]$ and
$E_2 = \dncast {\sigma_1} {\sigma_2} E$. By assumption on $M$ and $N$, will suffice to consider the following

* Let $k \le j$ and let $(V_1, V_2) \in \simivrel {A} {k}$.
We need to show

\[ ( E[\dncast {\sigma_1}{\sigma_2} V_1], \dncast {\sigma_1} {\sigma_2} E[V_2] ) \in
\simierel {\sigma_1} {k} {\simivrel {B} {}}. \]

By the operational semantics, we have $E[\dncast {\sigma_1}{\sigma_2} V_1] \stepsin 1 E[V_1]$.

By anti-reduction, it suffices to show

\[ ( E[V_1], \dncast {\sigma_1} {\sigma_2} E[V_2] ) \in
\simierel {\sigma_1} {k} {\simivrel {B} {}}. \]

Furthermore, there exist $i_1$ and $i_2$ and values $V_1'$ and $V_2'$ such that
$E[V_1] \stepsin {i_1} V_1'$ and
$E[V_2] \stepsin {i_2} V_2'$.

We also have $\dncast {\sigma_1} {\sigma_2} V_2' \stepsin 1 V_2'$.

Putting the above facts together, by anti-reduction, it suffices to show

\[ ( V_1', V_2' ) \in
\simierel {\sigma_1} {k} {\simivrel {B} {}}. \]

But by forward reduction, it suffices to show that
$(E[V_1], E[V_2]) \in \simierel {\sigma_1} {k} {\simivrel {B} {}}$.

For this, it suffices (by the congruence lemmas) that $V_1$ and $V_2$ are related,
which is true by assumption.

* Let $k \le j$ and let
$\effname @ c^r \leadsto d^r \in \sigma_2$ be an effect caught by
$\dncast {\sigma_1} {\sigma_2} \hole$.
Let $V^l, V^r, E^l\apart \effname, E^r \apart \effname$ be as in the statement of
Lemma <ref>.
We need to show

\[ ( E[\dncast {\sigma_1}{\sigma_2} E^l[\raiseOpwithM{\effname}{V^l}]],
\dncast {\sigma_1} {\sigma_2} E[E^r[\raiseOpwithM{\effname}{V^r}]] ) \in
\simierel {\sigma_1} {k} {\simivrel {B} {}}.
\]

If $\effname \notin \sigma_1$, then, by the operational semantics,
both terms will step to $\err$.
By anti-reduction, it suffices to show that
$(\err, \err) \in \simierel {\sigma_1} {k} {\simivrel {B} {}}$.
This follows by ErrBot (Lemma <ref>).

Now suppose $\effname @ c^l \leadsto d^l \in \sigma_1$.
According to the operational semantics, we have

\[
E[\dncast {\sigma_1}{\sigma_2}
E^l[\raiseOpwithM{\effname}{V^l}]] \stepsin 1
E[E^l[\upcast {d^l} {d^r}
\raiseOpwithM
\effname
{\dncast {c^l} {c^r} V^l}]],
\]

\[ \dncast {\sigma_1} {\sigma_2}
E[E^r[\raiseOpwithM\effname{V^r}]] \stepsin 1
E[E^r[\upcast {d^l} {d^r}
\raiseOpwithM
\effname
{\dncast {c^l} {c^r} V^r}]].
\]

Thus, by anti-reduction, it suffices to show

\begin{align*}
&E[E^l[\upcast {d^l} {d^r}
\raiseOpwithM
\effname
{\dncast {c^l} {c^r} V^l}]], \\
&E[E^r[\upcast {d^l} {d^r}
\raiseOpwithM
\effname
{\dncast {c^l} {c^r} V^r}]]
) \\
& \quad \quad \in \simierel {\sigma_1} {k} {\simivrel {B} {}}.
\end{align*}

Let $V'^l$ be the value to which $\dncast {c^l} {c^r} V^l$ steps, and similarly
let $V'^r$ be the value to which $\dncast {c^l} {c^r} V^r$ steps.
By anti-reduction, it suffices to show

\begin{align*}
&E[E^l[\upcast {d^l} {d^r}
\raiseOpwithM
\effname
{V'^l}]], \\
&E[E^r[\upcast {d^l} {d^r}
\raiseOpwithM
\effname
) \\
& \quad \quad \in \simierel {\sigma_1} {k} {\simivrel {B} {}}.
\end{align*}

As neither term steps, it is sufficient to show that they are related in
$\simirrel {\sigma_1} {k} {\simivrel {B} {}}$.
We assert the second disjunct in the definition of $\simirrel{\cdot}{}{}$,
taking $E^l = E[E^l[\upcast {d^l} {d^r} \hole]]$ and $E^r = E[E^r[\upcast {d^l} {d^r} \hole]]$.

We first need to show that $(V'^l, V'^r) \in (\later \simivrel {c} {})_k$.
By forward reduction, it suffices to show that

\[ (\dncast {c^l} {c^r} V^l, \dncast {c^l} {c^r} V^r)
\in (\later \simierel {\sigma_1} {} {})_{k} (\simivrel {c^r} {}). % TODO is the effect precision derivation correct?
\]

By monotonicity of casts (lemma <ref>), it suffices to show
$(V^l, V^r) \in (\later \simierel {\sigma_1} {} {})_{k} (\simivrel {c^r} {})$.
This follows from our assumption about $V^l$ and $V^r$.

We now need to show that

\[ ( x^l.E[E^l[\upcast {d^l} {d^r} x^l]], x^r.E[E^r[\upcast {d^l} {d^r} x^r]] )
\in (\later \simikrel {d} {} {})_{k} (\simierel {\sigma_1} {} {\simivrel {B} {}}).
\]

To this end, let $k' \le k$ and let $(V_1, V_2) \in (\later \simivrel {d^l})_{k'}$.
We need to show

\[
( E[E^l[\upcast {d^l} {d^r} V_1]], E[E^r[\upcast {d^l} {d^r} V_2]] ) \in
(\later \simierel {\sigma_1} {})_{k'} (\simivrel {B} {}).
\]

It will suffice by the soundness of the congruence rules to show that

\[
( E^l[\upcast {d^l} {d^r} V_1], E^r[\upcast {d^l} {d^r} V_2] ) \in
(\later \simierel {\sigma_1} {})_{k'} (\simivrel {B} {}).
\]

Let $V_1'$ and $V_2'$ be the values to which $\upcast {d^l} {d^r} V_1$ and
$\upcast {d^l} {d^r} V_2$ step, respectively. By anti-reduction, it suffices to show

\[
( E^l[V_1'], E^r[V_2'] ) \in
(\later \simierel {\sigma_1} {})_{k'} (\simivrel {B} {}).
\]

By assumption on $E^l$ and $E^r$, it suffices to show that
$(V_1', V_2') \in (\later \simivrel {d^r} {})_{k'}$.
By forward reduction, it suffices to show

\[
( \upcast {d^l} {d^r} V_1, \upcast {d^l} {d^r} V_2 ) \in
(\later \simierel {\sigma_1} {})_{k'} (\simivrel {B} {}).
\]

By monotonicity of casts (lemma <ref>), it suffices to show

\[
( V_1, V_2 ) \in
(\later \simierel {\sigma_1} {})_{k'} (\simivrel {B} {}).
\]

This follows from our assumption on $V_1$ and $V_2$.

Value casts commute with effect casts.

This follows from <ref>, because
$\upcast{A}{B} \hole$ and $\dncast{A}{B} \hole$
satisfy the requirements in the lemma.

Let $M$ be a term such that $\hastyDRhoMT{\cdot}{\sigma}{M}{A}$.
Let $c : A \ltdyn B$ and $e : B \ltdyn C$.
Let $d_\sigma : \sigma \ltdyn \sigma'$ and let $d_\sigma' : \sigma' \ltdyn \sigma''$

Suppose $\sg^\ltdyn \vDash_{\sigma} M \equiv N : A$.
Then the following hold:

Identity properties:
Suppose $\sg^\ltdyn \vDash_{\sigma} M \equidyn N : A$. We have

* $\sg \vDash_{\sigma} \upcast A A M \equiv N : A$

* $\sg \vDash_{\sigma} \dncast A A M \equiv N : A$

* $\sg \vDash_{\sigma} \upcast {\sigma} {\sigma} M \equiv N : A$

* $\sg \vDash_{\sigma} \dncast {\sigma} {\sigma} M \equiv N : A$

Composition properties:
Let $c : A \ltdyn B$ and $e : B \ltdyn C$.
Let $d_\sigma : \sigma \ltdyn \sigma'$ and $d_\sigma' : \sigma' \ltdyn \sigma''$.
Suppose $M \equidyn N$. Then

* $\sg \vDash_{\sigma} \upcast A C M \equidyn \upcast B C \upcast A B N : C$

* $\sg \vDash_{\sigma} \dncast A C M \equidyn \dncast A B \dncast B C N : A$

* $\sg \vDash_{\sigma''} \upcast {\sigma} {\sigma''} M \equidyn \upcast {\sigma'} {\sigma''} \upcast {\sigma} {\sigma'} N : A$

* $\sg \vDash_{\sigma} \dncast {\sigma} {\sigma''} M \equidyn \dncast {\sigma} {\sigma'} \dncast {\sigma'} {\sigma''} N : A$

We prove more general, “pointwise" versions of the above statements.
For instance, we show that if $(M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$,
then $(\upcast A A M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$.

Additionally, we only prove one direction of each of the equivalences (i.e., $\ltdyn$);
the proof of the other direction is symmetric.

The statements are proven simultaneously by induction on $A$ and $\sigma$.

* Identity properties:

* We need to show $(\upcast A A M, N) \in \simierel {\sigma} j {\simivrel A {}}$.
By monadic bind (Lemma <ref>), with $E_1 = \upcast A A \hole$ and $E_2 = \hole$,
it will suffice to show the following: Let $k \le j$ and $(V_1, V_2) \in \simivrel A k$. We will show

\[ (\upcast A A V_1, V_2) \in \simierel {\sigma} k {\simivrel A {}}. \]

We continue by induction on $A$. If $A = \boolty$, then we need to show

\[ (\upcast \boolty \boolty V_1, V_2) \in \simierel {d_\sigma} k {\simivrel \boolty {}}. \]

By anti-reduction, it suffices to show $(V_1, V_2) \in \simierel {\sigma} k {\simivrel {\boolty} {}}$,
which follows from our assumption on $(V_1, V_2)$.

If $A = A_i \to_{\sigma_A} A_o$, we need to show

\[ (\upcast {(A_i \to_{\sigma_A} A_o)} {(A_i \to_{\sigma_A} A_o)} V_1, V_2) \in
\simierel {\sigma} k {\simivrel {A_i \to_{\sigma_A} A_o} {}}. \]

As both terms are values, it suffices to show they are related in
$\simivrel {A_i \to_{\sigma_A} A_o} k$. So, let $k' \le k$ and let
$(V^l, V^r) \in \simivrel {A_i} {k'}$. We need to show

\[ ( (\upcast {(A_i \to_{\sigma_A} A_o)} {(A_i \to_{\sigma_A} A_o)} V_1)\, V^l,
V_2\, V^r ) \in
\simierel {\sigma_A} {k'} {\simivrel {A_o} {}}. \]

By anti-reduction, it suffices to show

\[
( \upcast {A_o} {A_o} \upcast {\sigma_A} {\sigma_A} (V_1\, \dncast {A_i} {A_i} V^l),
V_2\, V^r ) \in
\simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\]

By the induction hypothesis (applied twice), it suffices to show

\[
( (V_1\, \dncast {A_i} {A_i} V^l),
V_2\, V^r ) \in
\simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\]

By the soudness of function application, it suffices to show that
$(V_1, V_2) \in \simivrel {A_i \to_{\sigma_A} A_o} {k'}$ and
$(\dncast {A_i} {A_i} V^l, V^r) \in \simierel {\sigma_A} {k'} {\simivrel {A_i} {}}$.
The former is true by assumption and downward closure ($k' \le k$).
The latter is true by inductive hypothesis, since $V^l$ and $V^r$ are related.

* This is dual to the above.

* We prove this statement by Löb induction (Lemma <ref>).
That is, assume for all $(M', N') \in (\later \simierel {\sigma} {} {})_j ({\simivrel {A} {}})$, we have
$(\upcast \sigma \sigma M', N') \in (\later \simierel {\sigma} {} {})_j ({\simivrel A {}})$.
Let $(M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$.
We need to show $(\upcast \sigma \sigma M, N) \in \simierel {\sigma} j {\simivrel A {}}$.
By monadic bind (Lemma <ref>), with $E_1 = \upcast \sigma \sigma \hole$ and $E_2 = \hole$,
it will suffice to consider the following cases.

* Let $k \le j$ and let $(V_1, V_2) \in \simivrel A k$. We need to show

\[ (\upcast \sigma \sigma V_1, V_2) \in \simierel {\sigma} k {\simivrel c {}}. \]

Per the operational semantics, we have $\upcast \sigma \sigma V_1 \stepsin 1 V_1$, so by anti-reduction it
suffices to show $(V_1, V_2) \in \simierel {\sigma} k {\simivrel A {}}$, which follows by the
assumption that $(V_1, V_2) \in \simivrel A k$.

* Let $k \le j$ and let
$\effname @ c_\effname \leadsto d_\effname$ be an effect caught by
$\upcast \sigma \sigma \hole$ – i.e., $\effname @ c_\effname \leadsto d_\effname \in \sigma$.
Note that, as $\sigma$ is a reflexivity derivation, $c_\effname$ and $d_\effname$ are
also reflexivity derivations, i.e., $c_\effname^l = c_\effname^r$
and likewise for $d_\effname$. For simplicity, let $C = c_\effname^l$
and $D = d_\effname^l$.

Let $V^l, V^r, E^l\apart \effname, E^r \apart \effname$ be as in the statement of
Lemma <ref>.
We need to show

\begin{align*}
( & \upcast \sigma \sigma E^l[\raiseOpwithM\effname{V^l}],
E^r[\raiseOpwithM\effname{V^r}] )
\\ &\quad\quad \in \simierel {\sigma} k {\simivrel A {}}.
\end{align*}

According to the operational semantics, we have

\begin{align*}
&\upcast \sigma \sigma
E^l[\raiseOpwithM\effname{V^l}] \stepsin 1 \\
\letXbeboundtoYinZ
{\dncast {D} {D} \raiseOpwithM \effname {\upcast {C} {C} V^l}}
{\upcast \sigma \sigma E^l[x]}
\end{align*}

So, by anti-reduction it suffices to show that

\begin{align*}
{\dncast {D} {D} \raiseOpwithM \effname {\upcast {C} {C} V^l}}
{\upcast \sigma \sigma E^l[x]}, \\
) \\
& \quad \quad \in \simierel {\sigma} {k} {\simivrel A {}}.
\end{align*}

Let $V'^l$ be the term to which $\upcast {C} {C} V^l$ steps.
By anti-reduction, it suffices to show that

\begin{align*}
{\dncast {D} {D} \raiseOpwithM \effname {V'^l}}
{\upcast \sigma \sigma E^l[x]}, \\
&E^r[\raiseOpwithM \effname {V^r}]
) \\
& \quad \quad \in \simierel {\sigma} {k} {\simivrel A {}}.
\end{align*}

The above terms do not step, so it suffices to show that they are related in
$\simirrel {\sigma} {k} {\simivrel A {}}$.
To this end, we will first show that
$(V'^l, V^r) \in (\later \simivrel {C} {})_k$.
By forward reduction, it suffices to show that
$(\upcast {C} {C} V^l, V^r) \in (\later \simierel {\simivrel {C} {}} {})_{k}$.
By the induction hypothesis, it suffices to show that $(V^l, V^r) \in (\later \simivrel {C} {})_(k)$.

Now we will show that

\begin{align*}
( &x^l.
{\dncast {D} {D} x^l}
{\upcast \sigma \sigma E^l[x]}), \,
x^r.E^r[x^r] )
\\ &\quad\quad \in (\later \simikrel {D} {} {})_k (\simierel {\sigma} {} {\simivrel A {}}).
\end{align*}

Let $k' \le k$ and let $(V_1, V_2) \in (\later \simivrel {A} {})_{k'}$. We need to show

\begin{align*}
( &(\letXbeboundtoYinZ
{\dncast {D} {D} V_1}
{\upcast \sigma \sigma E^l[x]}), \,
\\ &\quad\quad \in (\later \simierel {\sigma} {} {})_{k'} ({\simivrel {A} {}}).
\end{align*}

Let $V_1'$ be the value to which $\dncast {D} {D} V_1$ steps.
By anti-reduction, it suffices to show

\begin{align*}
( &(\letXbeboundtoYinZ
{\upcast \sigma \sigma E^l[x]}), \,
\\ &\quad\quad \in (\later \simierel {\sigma} {} {})_{k'} ({\simivrel {A} {}}),
\end{align*}

and then since the let term steps, it suffices by anti-reduction again to show

\begin{align*}
( & {\upcast \sigma \sigma E^l[V_1']}, \,
E^r[V_2] )
\in (\later \simierel {\sigma} {} {})_{k'} ({\simivrel {A} {}}),
\end{align*}

By the Löb induction hypothesis, it suffices to show that

\[
(E^l[V_1'], E^r[V_2]) \in (\later \simierel {\sigma} {} {})_{k'} ({\simivrel {A} {}})
\]

By our assumption on $E^l$ and $E^r$, it suffices to show

\[
(V_1', V_2) \in
(\later \simivrel {A} {})_{k'}.
\]

By forward reduction, it suffices to show

\[
(\dncast {D} {D} V_1, V_2) \in
(\later \simivrel {A} {})_{k'}. % TODO step index
\]

By the induction hypothesis for value types, it suffices to show

\[
(V_1, V_2) \in
(\later \simierel {A} {})_{k'}.
\]

This follows by assumption.

* We again use Löb induction and monadic bind.

That is, assume for all $(M', N') \in (\later \simierel {\sigma} {} {})_j ({\simivrel {A} {}})$, we have
$(\dncast \sigma \sigma M', N') \in (\later \simierel {\sigma} {} {})_j ({\simivrel A {}})$. We need to show

\[ (\dncast \sigma \sigma M, N) \in \simierel {\sigma} j {\simivrel A {}} \]

where $(M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$.
We again use monadic bind, and as in the previous proof, the case of related values
follows trivially since effect casts are the identity on values.
Thus, it will suffice to show the related raises case.
That is, let $k \le j$ and let
$\effname @ c_\effname \leadsto d_\effname$ be an effect caught by
$\dncast \sigma \sigma \hole$ – i.e., $\effname @ c_\effname \leadsto d_\effname \in \sigma$.
As in the previous proof, since $\sigma$ is a reflexivity derivation, $c_\effname$ and $d_\effname$ are
also reflexivity derivations, so for simplicity, let $C = c_\effname^l = c_\effname^r$
and $D = d_\effname^l = d_\effname^r$.

Let $V^l, V^r, E^l\apart \effname, E^r \apart \effname$ be as in the statement of
the monadic bind lemma.
We need to show

\begin{align*}
( & \dncast \sigma \sigma E^l[\raiseOpwithM\effname{V^l}],
E^r[\raiseOpwithM \effname {V^r}] )
\\ &\quad\quad \in \simierel {\sigma} k {\simivrel A {}}.
\end{align*}

Note that, since $\effname \in \sigma$, the downcast cannot fail.

The remainder of the proof proceeds exactly like the previous proof,
with upcasts and downcasts interchanged.

* Composition properties:

* We need to show
$(\upcast A C M, \upcast B C \upcast A B N) \in \simierel {\sigma} {j} {\simivrel {C} {}}$.

By monadic bind (Lemma <ref>) with $E_1 = \upcast A C \hole$ and $E_2 = \upcast B C \upcast A B \hole$,
it will suffice to show the following: Let $k \le j$ and let $(V_1, V_2) \in \simivrel {A} {k}$.
We will show

\[ (\upcast A C V_1, \upcast B C \upcast A B V_2) \in \simierel {\sigma} {k} {\simivrel {C} {}}. \]

If $c \circ e = \boolty$, then $c = e = \boolty$, and we need to show

\[ (\upcast \boolty \boolty V_1, \upcast \boolty \boolty \upcast \boolty \boolty V_2) \in
\simierel {\sigma} {k} {\simivrel {\boolty} {}}. \]

By anti-reduction, it suffices to show $(V_1, V_2) \in \simivrel {\boolty} {j}$,
which follows from our assumption.

Now suppose $c \circ e = (c_i \circ e_i) \to_{(c_\sigma \circ e_\sigma)} (c_o \circ e_o)$.
We need to show

\begin{align*} (
&\upcast {(A_i \to_{\sigma_A} A_o)} {(C_i \to_{\sigma_C} C_o)} V_1, \\
&\upcast {(B_i \to_{\sigma_B} B_o)} {(C_i \to_{\sigma_C} C_o)}
\upcast {(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} V_2
) \\
&\quad\quad\quad\quad \in \simierel {\sigma} {k} {\simivrel {C_i \to_{\sigma_C} C_o} {}}.
\end{align*}

Both terms are values, so it suffices to show that they are related in
$\simivrel {C_i \to_{\sigma_C} C_o} {k}$.
Let $k' \le k$ and let $(V^l, V^r) \in \simivrel {C_i} {k'}$.
We need to show that

\begin{align*} (
&(\upcast {(A_i \to_{\sigma_A} A_o)} {(C_i \to_{\sigma_C} C_o)} V_1)\, V^l, \\
&(\upcast {(B_i \to_{\sigma_B} B_o)} {(C_i \to_{\sigma_C} C_o)}
\upcast {(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} V_2)\, V^r
) \\
&\quad\quad\quad\quad \in \simierel {\sigma_C} {k'} {\simivrel {C_o} {}}.
\end{align*}

By anti-reduction, it suffices to show

\begin{align*} (
&\upcast {A_o} {C_o} \upcast {\sigma_A} {\sigma_C} (V_1\, \dncast {A_i} {C_i} V^l), \\
&\upcast {B_o} {C_o} \upcast {\sigma_B} {\sigma_C} \\
&\quad\quad ((\upcast {(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} V_2)\, \dncast {B_i} {C_i} V^r)
) \\
&\quad\quad\quad\quad \in \simierel {\sigma_C} {k'} {\simivrel {C_o} {}}.
\end{align*}

Let $V'^r$ be the value to which $\dncast {B_i} {C_i} V^r$ steps.
By anti-reduction, it suffices to show

\begin{align*} (
&\upcast {A_o} {C_o} \upcast {\sigma_A} {\sigma_C} (V_1\, \dncast {A_i} {C_i} V^l), \\
&\upcast {B_o} {C_o} \upcast {\sigma_B} {\sigma_C} \\
&\quad\quad ((\upcast {(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} V_2)\, V'^r)
) \\
&\quad\quad\quad\quad \in \simierel {\sigma_C} {k'} {\simivrel {C_o} {}}.
\end{align*}

By anti-reduction again, it suffices to show

\begin{align*} (
&\upcast {A_o} {C_o} \upcast {\sigma_A} {\sigma_C} (V_1\, \dncast {A_i} {C_i} V^l), \\
&\upcast {B_o} {C_o} \upcast {\sigma_B} {\sigma_C} \\
&\quad\quad (\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V'^r))
) \\
&\quad\quad\quad\quad \in \simierel {\sigma_C} {k'} {\simivrel {C_o} {}}.
\end{align*}

We will appeal to transitivity (Lemma <ref>).
We continue by cases on $\sim$.

* First suppose $\sim \, =\, <$.  We first claim that

\begin{align*} (
&\upcast {A_o} {C_o} \upcast {\sigma_A} {\sigma_C} (V_1\, \dncast {A_i} {C_i} V^l), \\
&\upcast {B_o} {C_o} \upcast {A_o} {B_o} \\
&\quad\quad (\upcast {\sigma_B} {\sigma_C} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V'^r))
) \\
&\quad\quad\quad\quad \in \simierel {\sigma_C} {k'} {\simivrel {C_o} {}}.
\end{align*}

By the induction hypothesis applied twice, it suffices to show

\begin{align*} (
&(V_1\, \dncast {A_i} {C_i} V^l), (V_2\, \dncast {A_i} {B_i} V'^r)
) \\
&\quad\quad\quad\quad \in \simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\end{align*}

By soundness of function application, it suffices to show that
$(V_1, V_2) \in \simivrel {A_i \to_{\sigma_A} A_o} {k'}$ and that

\[ (\dncast {A_i} {C_i} V^l, \dncast {A_i} {B_i} V'^r)
\in \simierel {\sigma} {k'} {\simivrel {A_i} {}}. \]

The former holds by assumption and downward closure. To show the latter, it suffices by
forward reduction to show that

\[ (\dncast {A_i} {C_i} V^l, \dncast {A_i} {B_i} \dncast {B_i} {C_i} V^r)
\in \simierel {\sigma} {k'} {\simivrel {A_i} {}}. \]

Now, by the induction hypothesis, it suffices to show that

\[ (V^l, V^r)
\in \simierel {\sigma} {k'} {\simivrel {C_i} {}}, \]

which follows from our assumption.

Now by transitivity, it will suffice to show

\begin{align*} (
&\upcast {B_o} {C_o} \upcast {A_o} {B_o} \\
&\quad\quad (\upcast {\sigma_B} {\sigma_C} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V'^r)), \\
&\upcast {B_o} {C_o} \upcast {\sigma_B} {\sigma_C} \\
&\quad\quad (\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V'^r))
) \\
&\quad\quad\quad\quad \in \gtierel {\sigma_C} {\omega} {\simivrel {C_o} {}}.
\end{align*}

By reflexivity (Corollary <ref>), we have
that $\upcast {A_o} {B_o} \upcast {\sigma_B} {\sigma_C} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V'^r)$
is related to itself.
Then by commutativity of casts (Corollary <ref>), we can interchange the order of
$\upcast {A_o} {B_o}$ and $\upcast {\sigma_B} {\sigma_C}$, and the resulting terms are related.
Finally by monotonicity of casts (Lemma <ref>), we can apply $\upcast {B_o} {C_o}$,
and the resulting terms are still related. Moreover, all of these relations hold “at $\omega"$.

* Now suppose $\sim \, = \, >$. By similar reasoning as in the previous case, we have

\begin{align*} (
&\upcast {A_o} {C_o} \upcast {\sigma_A} {\sigma_C} (V_1\, \dncast {A_i} {C_i} V^l), \\
&\upcast {B_o} {C_o} \upcast {A_o} {B_o} \\
&\quad\quad (\upcast {\sigma_B} {\sigma_C} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V^l))
) \\
&\quad\quad\quad\quad \in \simierel {\sigma_C} {\omega} {\simivrel {C_o} {}}.
\end{align*}

Thus, by transitivity it will suffice to show

\begin{align*} (
&\upcast {B_o} {C_o} \upcast {A_o} {B_o} \\
&\quad\quad (\upcast {\sigma_B} {\sigma_C} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V^l)), \\
&\upcast {B_o} {C_o} \upcast {\sigma_B} {\sigma_C} \\
&\quad\quad (\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V'^r))
) \\
&\quad\quad\quad\quad \in \gtierel {\sigma_C} {k'} {\simivrel {C_o} {}}.
\end{align*}

The reasoning is analogous to that of the previous case.

* This is dual to the above.

* We prove this statement by Löb induction (Lemma <ref>).
That is, assume for all $(M', N') \in (\later \simierel {\sigma} {} {})_j ({\simivrel {A} {}})$, we have

\[ (\upcast {\sigma} {\sigma''} M, \upcast {\sigma'} {\sigma''} \upcast {\sigma} {\sigma'} N)
\in (\later \simierel {\sigma''} {} {})_{j} ({\simivrel {A} {}}).
\]

Let $(M, N) \in \simierel {\sigma} {j} {\simivrel {A} {}}$.
We need to show

\[ (\upcast {\sigma} {\sigma''} M, \upcast {\sigma'} {\sigma''} \upcast {\sigma} {\sigma'} N)
\in \simierel {\sigma''} {j} {\simivrel {A} {}}.
\]

By monadic bind (Lemma <ref>), with
$E_1 = \upcast {\sigma} {\sigma''} \hole$
and $E_2 = \upcast {\sigma'} {\sigma''} \upcast {\sigma} {\sigma'} \hole$,
it suffices to consider the follwing cases:

* Let $k \le j$ and let $(V_1, V_2) \in \simivrel {A} {k}$. We need to show that

\[ (\upcast {\sigma} {\sigma''} V_1, \upcast {\sigma'} {\sigma''} \upcast {\sigma} {\sigma'} V_2)
\in \simierel {\sigma''} {j} {\simivrel {A} {}}.
\]

Since the effect cast is the identity on values, the above follows immediately
by anti-reduction.

* Let $k \le j$ and let
$\effname @ c_\effname \leadsto d_\effname \in \sigma$ be an effect caught by either $E_1$ or $E_2$.
Note that, as $\sigma$ is a reflexivity derivation, $c_\effname$ and $d_\effname$ are
also reflexivity derivations, i.e., $c_\effname^l = c_\effname^r$
and likewise for $d_\effname$. For simplicity, let $C^L = c_\effname^l$
and $D^L = d_\effname^l$.

Let $V^l, V^r, E^l\apart \effname, E^r \apart \effname$ be as in the statement of
the monadic bind lemma.
We need to show

\begin{align*} (
&\upcast {\sigma} {\sigma''}
E^l [\raiseOpwithM \effname {V^l}], \\
&\upcast {\sigma'} {\sigma''} \upcast {\sigma} {\sigma'}
E^r[\raiseOpwithM \effname {V^r}]
) \\
&\quad \quad \in \simierel {\sigma''} {k} {\simivrel {A} {}}.
\end{align*}

Let $C^M$ and $D^M$ be the types such that $\effname @ C^M \leadsto D^M \in \sigma'$
Let $C^R$ and $D^R$ be the types such that $\effname @ C^R \leadsto D^R \in \sigma''$.
By anti-reduction, it suffices to show

\begin{align*}
{\dncast {D^L} {D^R} \raiseOpwithM\effname{\upcast {C^L} {C^R} V^l}}
{\upcast {\sigma} {\sigma''} E^l[x]}, \\
&\upcast {\sigma'} {\sigma''}
{\dncast {D^L} {D^M} \raiseOpwithM\effname{\upcast {C^L} {C^M} V^r}}
{\upcast {\sigma} {\sigma'} E^r[x]})
) \\
&\quad\quad \in \simierel {\sigma''} {k} {\simivrel {A} {}}.
\end{align*}

Let $V'^l$ be the value to which $\upcast {C^L} {C^R} V^l$ steps, say in $i$ steps.
Let $V'^r$ be the value to which $\upcast {C^L} {C^M} V^r$ steps, say in $j$ steps.

By anti-reduction, it suffices to show

\begin{align*}
{\dncast {D^L} {D^R} \raiseOpwithM\effname{V'^l}}
{\upcast {\sigma} {\sigma''} E^l[x]}, \\
&\upcast {\sigma'} {\sigma''}
{\dncast {D^L} {D^M} \raiseOpwithM\effname{V'^r}}
{\upcast {\sigma} {\sigma'} E^r[x]})
) \\
&\quad\quad \in \simierel {\sigma''} {k} {\simivrel {A} {}}.
\end{align*}

Now (taking $E' = \letXbeboundtoYinZ{\dncast {D^L} {D^M} \hole}{x}{\upcast {\sigma} {\sigma'} E^r[x]}$
in the EffUpCast rule), it will suffice by anti-reduction to show

\begin{align*}
{\dncast {D^L} {D^R} \raiseOpwithM\effname{V'^l}}
{\upcast {\sigma} {\sigma''} E^l[x]}, \\
{\dncast {D^M} {D^R}
\raiseOpwithM\effname{\upcast {C^M} {C^R} V'^r}}
{\\ & \quad \upcast {\sigma'} {\sigma''}
{\dncast {D^L} {D^M} y}
{\upcast {\sigma} {\sigma'} E^r[x]})
) \\
&\quad\quad \in \simierel {\sigma''} {k} {\simivrel {A} {}}.
\end{align*}

Let $V''^r$ be the value to which $\upcast {C^M} {C^R} V'^r$ steps.

By anti-reduction, it suffices to show

\begin{align*}
{\dncast {D^L} {D^R} \raiseOpwithM \effname {V'^l}}
{\upcast {\sigma} {\sigma''} E^l[x]}, \\
{\dncast {D^M} {D^R}
\raiseOpwithM \effname {V''^r}}
{\\ & \quad \upcast {\sigma'} {\sigma''}
{\dncast {D^L} {D^M} y}
{\upcast {\sigma} {\sigma'} E^r[x]})
) \\
&\quad\quad \in \simierel {\sigma''} {k} {\simivrel {A} {}}.
\end{align*}

As neither term steps, we will show that they belong to $\simirrel {\sigma''} {k} {\simivrel {A} {}}$.
We first need to show that

\[
(V'^l, V''^r) \in (\later \simivrel {A} {})_k.
\]

By forward-reduction, it suffices to show that

\[
(\upcast {C^L} {C^R} V^l, \upcast {C^M} {C^R} \upcast {C^L} {C^M} V^r) \in
(\later \simivrel {A} {})_k.
\]

By the induction hypothesis for value types, it suffices to show that
$(V^l, V^r) \in (\later \simivrel {A} {})_k$, which is true by assumption.

Now we need to show that, for all $k' \le k$ and related values
$(V_1, V_2) \in (\later \simivrel {A} {})_{k'}$, we have

\begin{align*}
{\dncast {D^L} {D^R} V_1}
{\upcast {\sigma} {\sigma''} E^l[x]}, \\
{\dncast {D^M} {D^R} V_2}
{\\ & \quad \upcast {\sigma'} {\sigma''}
{\dncast {D^L} {D^M} y}
{\upcast {\sigma} {\sigma'} E^r[x]})
) \\
&\quad\quad \in (\later \simierel {\sigma''} {} {})_{k'} ({\simivrel {A} {}}).
\end{align*}

Let $V_1'$ and $V_2'$ be the values to which $\dncast {D^L} {D^R} V_1$
and $\dncast {D^M} {D^R} V_2$ step, respectively. By anti-reduction, it
will suffice to show

\begin{align*}
&{\upcast {\sigma} {\sigma''} E^l[V_1']}, \\
&{\upcast {\sigma'} {\sigma''}
{\dncast {D^L} {D^M} V_2'}
{\upcast {\sigma} {\sigma'} E^r[x]})
) \\
&\quad\quad \in (\later \simierel {\sigma''} {} {})_{k'} ({\simivrel {A} {}}).
\end{align*}

Let $V_2''$ be the value to which $\dncast {D^L} {D^M} V_2'$ steps. By anti-reduction,
it will suffice to show

\begin{align*}
&{\upcast {\sigma} {\sigma''} E^l[V_1']}, \\
&{\upcast {\sigma'} {\sigma''}
({\upcast {\sigma} {\sigma'} E^r[V_2'']})
) \\
&\quad\quad \in (\later \simierel {\sigma''} {} {})_{k'} ({\simivrel {A} {}}).
\end{align*}

Now by the Löb induction hypothesis, it suffices to show

\begin{align*}
&{E^l[V_1']}, {E^r[V_2'']}
\in (\later \simierel {\sigma''} {} {})_{k'} ({\simivrel {A} {}}).
\end{align*}

By assumption on $E^l$ and $E^r$, it suffices to show

\begin{align*}
&V_1', V_2''
\in (\later \simivrel {A} {})_{k'}.
\end{align*}

Now by forward reduction it suffices to show

\begin{align*}
& \dncast {D^L} {D^R} V_1,
\dncast {D^L} {D^M} \dncast {D^M} {D^R} V_2
\in (\later \simierel {\sigma''} {} {})_{k'} (\simivrel {A} {}).
\end{align*}

This follows by the inductive hypothesis for value types and our assumption on
$V_1$ and $V_2$.

* This is dual to the above: we use Löb induction and monadic bind,
and we reach a point where we need to show

\begin{align*} (
&\dncast {\sigma} {\sigma''}
E^l [\raiseOpwithM \effname {V^l}], \\
&\dncast {\sigma'} {\sigma''} \dncast {\sigma} {\sigma'}
E^r[\raiseOpwithM \effname {V^r}]
) \\
&\quad \quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

where $\effname @ C^R \leadsto D^R \in \sigma''$.

If $\effname \notin \sigma$, then the left-hand side steps to $\err$, as does the right-hand side.
By ErrBot (Lemma <ref>), $\err$ is related to itself, so by anti-reduction, we are finished.
If $\effname \notin \sigma'$, then in fact, $\effname \notin \sigma$ (since $\sigma \ltdyn \sigma'$),
and so again, both sides step to $\err$.

Otherwise, we proceed as in the proof of the previous case, with
the upcasts and downcasts interchanged.

Let $c : A \ltdyn B$, and $d_\sigma : \sigma \ltdyn \sigma'$, and let $M$ and $N$
be terms such that $\sg^\ltdyn \vDash_{\sigma} M \ltdyn N : A$.
The following hold:

* $\sg^\ltdyn \vDash_{\sigma} \upcast {A} {B} M \ltdyn \upcast {A} {B} N : B$

* $\sg^\ltdyn \vDash_{\sigma} \dncast {A} {B} M \ltdyn \dncast {A} {B} N : A$

* $\sg^\ltdyn \vDash_{\sigma'} \upcast {\sigma} {\sigma'} M \ltdyn \upcast {\sigma} {\sigma'} N : A$

* $\sg^\ltdyn \vDash_{\sigma} \dncast {\sigma} {\sigma'} M \ltdyn \dncast {\sigma} {\sigma'} N : A$

As in the proof of the functoriality properties of casts, we prove
stronger, “pointwise” versions of the above statements, i.e., we assume
$(M, N) \in \simierel {\sigma} {j} {\simivrel A {}}$, and show, for example, that
$(\upcast A B M, \upcast A B N) \in \simierel {\sigma} {j} {\simivrel {B} {}}$.

The proof is by induction on $c$ and $d_\sigma$.

* We need to show

\[ (\upcast A B M, \upcast A B N) \in \simierel {\sigma} {j} {\simivrel B {}}. \]

By monadic bind (Lemma <ref>), with $E_1 = E_2 = \upcast A B \hole$,
it will suffice to show that

\[ (\upcast A B {V_1}, \upcast A B {V_2}) \in \simierel {\sigma} {k} {\simivrel B {}}, \]

where $k \le j$ and let $(V_1, V_2) \in \simivrel A k$.

If $c = \boolty$, then we need to show

\[ (\upcast \boolty \boolty {V_1}, \upcast \boolty \boolty {V_2}) \in
\simierel {\sigma} {k} {\simivrel \boolty {}}. \]

By anti-reduction, it suffices to show that
$(V_1, V_2) \in \simierel {\sigma} {k} {\simivrel \boolty {}}$,
which follows from our assumption.

If $c = c_i \to_{c_\sigma} c_o$, then we need to show

\begin{align*} (
&\upcast {(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} {V_1}, \,
\upcast {(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} {V_2})
\\ & \quad \quad \in \simierel {\sigma} {k} {\simivrel {B_i \to_{\sigma_B} B_o} {}}.
\end{align*}

As both terms are values, it suffices to show that they are related in
$\simivrel {B_i \to_{\sigma_B} B_o} k$.
Let $k' \le k$ and let $(V^l, V^r) \in \simikrel {B_i} {k'}$.
We need to show

\begin{align*}
( &(\upcast {(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} {V_1})\, V^l, \\
&(\upcast {(A_i \to_{\sigma_A} A_o)} {(B_i \to_{\sigma_B} B_o)} {V_2})\, V^r )
\\ & \quad \quad \in \simierel {\sigma_B} {k'} {\simivrel {B_o} {}}.
\end{align*}

By anti-reduction, it suffices to show

\begin{align*}
( &\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} (V_1\, \dncast {A_i} {B_i} V^l) , \\
&\upcast {A_o} {B_o} \upcast {\sigma_A} {\sigma_B} (V_2\, \dncast {A_i} {B_i} V^r)
) \\ & \quad \quad \in \simierel {\sigma_B} {k'} {\simivrel {B_o} {}}.
\end{align*}

By the inductive hypothesis applied twice, it suffices to show

\[
( (V_1\, \dncast {A_i} {B_i} V^l) ,
(V_2\, \dncast {A_i} {B_i} V^r)
) \in \simierel {\sigma_A} {k'} {\simivrel {A_o} {}}.
\]

By soundness of function application, it suffices to show that $(V_1, V_2) \in \simivrel {A_i \to_{\sigma_A} A_o} {k'}$
and that $(\dncast {A_i} {B_i} V^l, \dncast {A_i} {B_i} V^r) \in \simierel {\sigma} {k'} {\simivrel {A_i} {}}$.
The former is true by our assumption about $V_1$ and $V_2$.
To show the latter, it suffices by the inductive hypothesis to show that
$(V^l, V^r) \in \simierel {\sigma} {k'} {\simivrel {B_i} {}}$, which follows by our assumption.

* This is dual to the above.

* This is dual to the below, and in fact easier since these are upcasts.

* We prove this statement by Löb induction (Lemma <ref>).
That is, assume for all
$(M', N') \in (\later \simierel {\sigma'} {} {})_j ({\simivrel {A} {}})$, we have

\[
(\dncast {\sigma} {\sigma'} M, \dncast {\sigma} {\sigma'} N) \in
(\later \simierel {\sigma} {} {})_j ({\simivrel A {}}).
\]

Let $(M, N) \in \simierel {\sigma'} {j} {\simivrel {A} {}}$.
We need to show

\[ (\dncast {\sigma} {\sigma'} M, \dncast {\sigma} {\sigma'} N) \in
\simierel {\sigma} {j} {\simivrel {A} {}}.
\]

By monadic bind (Lemma <ref>), it will suffice to consider
the following two cases:

* Let $k \le j$ and let $(V_1, V_2) \in \simivrel {A} {k}$. We need to show that

\[
(\dncast {\sigma} {\sigma'} V_1, \dncast {\sigma} {\sigma'} V_2) \in
\simierel {\sigma} {j} {\simivrel {A} {}}.
\]

Since the effect cast is the identity on values, the above follows immediately
by anti-reduction.

* Let $k \le j$ and let
$\effname @ c_\effname \leadsto d_\effname \in \sigma'$ be an effect caught by
$\dncast {\sigma} {\sigma'} \hole$. Recalling that $\sigma'$ is shorthand for the
reflexivity derivation $\sigma' \ltdyn \sigma'$, we have that $c_\effname$ and $d_\effname$
are themselves reflexivity (type precision) derivations; for brevity, we
refer to the types as $C$ and $D$.

Let $(V^l, V^r) \in (\later \simivrel {C} {})_{k}$ and
and let $E^l\apart \effname, E^r \apart \effname$ be such that

\[
(x^l.E^l[x^l], x^r.E^r[x^r]) \in
(\later \simikrel {D} {})_{k} (\simierel {\sigma} {} {\simivrel {A} {}}).
\]

We need to show

\begin{align*}
(&\dncast {\sigma} {\sigma'} E^l[\raiseOpwithM \effname {V^l}], \\
&\dncast {\sigma} {\sigma'} E^r[\raiseOpwithM \effname {V^r}])
\\ &\quad \quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

First, if $\effname \notin \sigma$, then both sides step to $\err$, and we are finished
by anti-reduction since $\err$ is related to itself by ErrBot (Lemma <ref>).

Otherwise, by anti-reduction, it suffices to show

\begin{align*}
{\upcast {D} {D} \raiseOpwithM \effname {\dncast {C} {C} V^l}}
{\dncast {\sigma} {\sigma'} E^l[x]}, \\
{\upcast {D} {D} \raiseOpwithM \effname {\dncast {C} {C} V^r}}
{\dncast {\sigma} {\sigma'} E^r[x]}
) \\
& \quad \quad \quad \quad \in (\later \simierel {\sigma} {} {})_{k} {(\simivrel {A} {})}.
\end{align*}

By the soundness of the term precision congruence rule for let, it suffices to show that (1)

\begin{align*}
&{\upcast {D} {D} \raiseOpwithM\effname{\dncast {C} {C} V^l}}, \\
&{\upcast {D} {D} \raiseOpwithM \effname {\dncast {C} {C} V^r}}
) \\
& \quad \quad \in (\later \simierel {\sigma} {} {})_{k} ({\simivrel {A} {}}).
\end{align*}

and (2) for all related $(V_1, V_2) \in (\later \simivrel {A} {})$, we have

\begin{align*}
&\dncast {\sigma} {\sigma'} E^l[V_1],
\dncast {\sigma} {\sigma'} E^r[V_2]
) \\
& \quad \quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

§.§.§ Transitivity

We introduce the following notation. We define $(M_1, M_2) \in R_\omega$ to mean that
$(M_1, M_2) \in R_k$ for all natural numbers $k$.

We now state and prove a “mixed transitivity” lemma, in which we allow
one of the two relations in the assumption to occur at a “proper" precision derivation,
while the other is constrained to occur at a reflexivity derivation.

If (1) $(M_1, M_2) \in \gtierel {\sigma} {\omega} {\gtivrel A {}}$ and
(2) $(M_2, M_3) \in \gtierel {d_\sigma} {j} {\gtivrel c {}}$,
then $(M_1, M_3) \in \gtierel {d_\sigma} j {\gtivrel c {}}$.

Similarly, if $(M_1, M_2) \in \ltierel {d_\sigma} {j} {\ltivrel c {}}$ and
$(M_2, M_3) \in \ltierel {\sigma} {\omega} {\ltivrel A {}}$,
then $(M_1, M_3) \in \ltierel {d_\sigma} j {\ltivrel c {}}$.

This is proved simultaneuously with the following two lemmas on transitivity
for results and values.
We prove the lemma for $\sim = >$; the other case is similar.

The proof is by Löb-induction (Lemma <ref>).
That is, assume that for all $M_1', M_2'$, and $M_3'$,
if $(M_1', M_2') \in (\later \gtierel {\sigma} {})_{\omega} (\gtivrel A {})$ and
$(M_2', M_3') \in (\later \gtierel {d_\sigma} {})_{j} (\gtivrel c {})$,
then $(M_1', M_3') \in (\later \gtierel {d_\sigma} {})_{j} (\gtivrel c {})$.

We proceed by considering cases on the assumption that
$(M_2, M_3) \in \gtierel {d_\sigma} {j} {\gtivrel c {}}$.

In the first case, $M_3 \stepsin {j+1}$. Then we immediately have that
$(M_1, M_3) \in \gtierel {d_\sigma} j {\gtivrel c {}}$, via the first disjunct.

In the second case, there is $k \le j$ such that $M_3 \stepsin {j - k} \err$
and $M_2 \stepsin s \err$, for some number of steps $s$.
By assumption (1), we have that $(M_1, M_2) \in \gtierel {\sigma} {s} {\gtivrel A {}}$.
By inversion, we see that the second disjunct must have been
true (with $k = 0$).
This means in particular that $M_1 \stepsin * \err$.
Thus, we may conclude using the second disjunct that
$(M_1, M_3) \in \gtierel {d_\sigma} j {\gtivrel c {}}$.

In the third case, there is $k \le j$ and $N_3$ such that $M_3 \stepsin {j - k} N_3$,
and $M_2 \stepsin s \err$, for some number of steps $s$.
By similar reasoning to the previous case, we may conclude using the third
disjunct that
$(M_1, M_3) \in \gtierel {d_\sigma} j {\gtivrel c {}}$.

Finally, in the fourth case, there exist $k \le j$ and
$(N_2, N_3) \in \gtirrel {d_\sigma} {k} {\gtivrel c {}}$
such that $M_2 \stepsin s N_2$ for some $s$, and $M_3 \stepsin {j - k} N_3$.
By assumption (1), we have that $(M_1, M_2) \in \gtierel {\sigma} {s + i} {\gtivrel A {}}$
for all $i \in \mathbb{N}$.
By inversion, we see that either the third or the fourth disjunct was true,
with $k = i$ in both cases (notice that $(s + i) - i = s$,
which is precisely the number of steps that $M_2$ takes to $N_2$).

In the former case, we have $M_1 \stepsin * \err$ and we can then finish by
asserting the third disjunct. In the latter case, there exists $N_1$ such that
$M_1 \stepsin * N_1$ and $(N_1, N_2) \in \gtirrel {\sigma} {i} {\gtivrel {A} {}}$.
Since $i$ is arbitrary, this tells us that
$(N_1, N_2) \in \gtirrel {\sigma} {\omega} {\gtivrel {A} {}}$.
To recap, we have
$(N_1, N_2) \in \gtirrel {\sigma} {\omega} {\gtivrel {A} {}}$,
and $(N_2, N_3) \in \gtirrel {d_\sigma} {k} {\gtivrel c {}}$, for some $k \le j$.
We want to show that $(N_1, N_3) \in \gtirrel {d_\sigma} {k} {\gtivrel c {}}$.

This follows from Lemma <ref>.

If $(V_1, V_2) \in {\gtivrel A {\omega}}$ and
$(V_2, V_3) \in {\gtivrel c {j}}$,
then $(V_1, V_3) {\gtivrel c {j}}$.

Similarly, if $(V_1, V_2) \in {\ltivrel c {j}}$ and
$(V_2, V_3) \in {\ltivrel A {\omega}}$,
then $(V_1, V_3) {\ltivrel c {j}}$.

Proved simultaneously with the homogeneous transitivity for terms
(Lemma <ref>) and for results (Lemma
The proof is by induction on the type precision derivation $c$.
We prove the first statement only; the other is proved similarly.

* Case $c = \boolty$. Then we have $V_1 = V_2 = V_3$ and either all are
$\tru$, or all are $\fls$. In either case, $V_1$ is related to $V_3$.

* Case $c = c_i \to_{c_\sigma} c_o$. Then $A = A_i \to_{\sigma_A} A_o$
and $B = B_i \to_{\sigma_B} B_o$.

We have
$(V_1, V_2) \in \simivrel {A_i \to_{\sigma_A} A_o} {\omega}$ and
$(V_2, V_3) \in \simivrel {c_i \to_{c_\sigma} c_o} {k}$.

We need to show

\[ (V_1, V_3) \in {\gtivrel {c_i \to_{c_\sigma} c_o} {j}}. \]

Let $k \le j$ and let $(V^l, V^r) \in \gtivrel {c_i} k$.
We need to show that

\[ (V_1\, V^l, V_3\, V^r) \in \gtierel {c_\sigma} {k} {\gtivrel {c_o} {}}. \]

By reflexivity (<ref>), we know that
$(V^l, V^l) \in \gtivrel {A_i} {\omega}$.

From our assumption about $(V_1, V_2)$, it follows that

\[ (V_1\, V^l, V_2\, V^l) \in \gtierel {\sigma_A} {\omega} {\gtivrel {A_o} {}}. \]

From our assumption about $(V_2, V_3)$, we have

\[ (V_2\, V^l, V_3\, V^r) \in \gtierel {c_\sigma} {k} {\gtivrel {c_o} {}}. \]

Now we apply the induction hypothesis (Lemma <ref>)
to conclude that

\[ (V_1\, V^l, V_3\, V^r) \in \gtierel {c_\sigma} {k} {\gtivrel {c_o} {}}, \]

as needed.

If (1) $(N_1, N_2) \in \gtirrel {\sigma} {\omega} {\gtivrel A {}}$ and
(2) $(N_2, N_3) \in \gtirrel {d_\sigma} {j} {\gtivrel c {}}$,
then $(N_1, N_3) \in \gtirrel {d_\sigma} j {\gtivrel c {}}$.

Similarly, if $(N_1, N_2) \in \ltirrel {d_\sigma} {j} {\ltivrel c {}}$ and
$(N_2, N_3) \in \ltirrel {\sigma} {\omega} {\ltivrel A {}}$,
then $(N_1, N_3) \in \ltirrel {d_\sigma} j {\ltivrel c {}}$.

We prove only the first statement; the second is analogous.

Let $j$ be fixed. We consider cases on assumption (1).
There are two subcases to consider. First, $N_1$ and $N_2$ are values
and $(N_1, N_2) \in \gtivrel A {\omega}$.
Then $N_3$ is also a value, and $(N_2, N_3) \in \gtivrel c {j}$.
By <ref>, we have that $(N_1, N_3) \in \gtivrel A {j}$.

Otherwise, there exist $\effname @ C \leadsto D \in \sigma$, $E_1 \apart epsilon$ and
$E_2 \apart \effname$, and $V_1$ and $V_2$ such that
$(V_1, V_2) \in (\later \gtivrel {C} {})_{\omega}$, and
$(x_1.E_1[x_1], x_2.E_2[x_2]) \in
(\later \gtikrel {D} {} {})_{\omega} (\gtierel {\sigma} {} {\gtivrel {A} {}})$, and

\[
N_1 = E_1[\raiseOpwithM{\effname}{V_1}],
\]

\[
N_2 = E_2[\raiseOpwithM{\effname}{V_2}].
\]

Similarly, since $N_2$ and $N_3$ are related in $\gtirrel {d_\sigma} {j} {\gtivrel c {}}$,
it follows that $\effname @ c_\effname \leadsto d_\effname \in d_\sigma$, where
$c_\effname : C \ltdyn C'$ and $d_\effname : D \ltdyn D'$.
We also know that there exist $E_3 \apart \effname$ and $V_3$ such that
$(V_2, V_3) \in (\later \gtivrel {c_\effname} {})_{j}$, and
$(x_2.E_2[x_2], x_3.E_3[x_3]) \in
(\later \gtikrel {d_\effname} {} {})_{j} (\gtierel {d_\sigma} {} {\gtivrel {c} {}})$, and

\[
N_3 = E_3[\raiseOpwithM{\effname}{V_3}].
\]

Recall that we need to show

\[
( E_1[\raiseOpwithM{\effname}{V_1}], E_3[\raiseOpwithM{\effname}{V_3}] ) \in
\gtirrel {d_\sigma} {j} {\gtivrel c {}}.
\]

We assert the second disjunct in the definition of $\gtirrel{\cdot}{}{}$.

We first claim that $(V_1, V_3) \in (\later \gtivrel {c_\effname} {})_{j}$.
By transitivity for values (Lemma <ref>), it suffices to show
that $(V_1, V_2) \in (\later \gtivrel {c_\effname} {})_{\omega}$ and
$(V_2, V_3) \in (\later \gtivrel {c_\effname} {})_{j}$. These follow by assumption.

Now we claim that

\[
(x_1.E_1[x_1], x_3.E_3[x_3]) \in
(\later \gtikrel {d_\effname} {} {})_{j} (\gtierel {d_\sigma} {} {\gtivrel {c} {}}).
\]

Let $k \le j$ and let $(V^l, V^r) \in (\later \gtivrel {d_\effname} {})_{k}$. We need to show

\[
(E_1[V^l], E_3[V^r]) \in (\later \gtierel {d_\sigma} {} {})_{k} (\gtivrel {c} {}).
\]

By the induction hypothesis (recall we are proving this simultaneously with transitivity
for terms, which is being proven by Löb induction), it suffices to find a term $M$ such that
$(E_1[V^l], M) \in (\later \gtierel {\sigma} {} {})_{\omega} (\gtivrel {A} {})$, and
$(M, E_3[V_r]) \in (\later \gtierel {d_\sigma} {} {})_{k} (\gtivrel {c} {})$.

By reflexivity (Corollary <ref>), we have
$(V^l, V^l) \in (\later \simivrel {} {})_{\omega}$.

Then by our assumption on $(E_1, E_2)$, we have

\[
(E_1[V^l], E_2[V^l]) \in (\later \gtierel {\sigma} {} {})_{\omega} (\gtivrel {A} {})
\]

By our assumption on $(E_2, E_3)$ we have

\[
(E_2[V^l], E_3[V^r]) \in (\later \gtierel {d_\sigma} {} {})_{k} (\gtivrel {c} {}),
\]

which finishes the proof.

Let $c : A_1 \ltdyn A_2$ and $e : A_2 \ltdyn A_3$.
Let $d_\sigma : \sigma \ltdyn \sigma'$ and let $d_\sigma' : \sigma' \ltdyn \sigma''$.

If (1) $(M_1, M_2) \in \gtierel {d_\sigma} {\omega} {\gtivrel c {}}$ and
(2) $(M_2, M_3) \in \gtierel {d_\sigma'} {j} {\gtivrel e {}}$,
then $(M_1, M_3) \in \gtierel {d_\sigma \circ d_\sigma'} j {\gtivrel {c \circ e} {}}$.

Similarly, if $(M_1, M_2) \in \ltierel {d_\sigma} {j} {\ltivrel c {}}$ and
$(M_2, M_3) \in \ltierel {d_\sigma'} {\omega} {\ltivrel e {}}$,
then $(M_1, M_3) \in \ltierel {d_\sigma \circ d_\sigma'} j {\ltivrel {c \circ e} {}}$.

Follows from mixed transitivity (Lemma <ref>) and
the generalized cast lemmas (Lemmas
<ref>, <ref>,
<ref>, <ref>,
<ref>, <ref>,
<ref>, and <ref>

For example, by EffDnR and ValDnR, we have

\[
(M_1,\, \dncast {\sigma} {\sigma'} \dncast {A_1} {A_2} M_2)
\in \gtierel {\sigma} {\omega} {\gtivrel {A_1} {}},
\]

and by EffDnL and ValDnL, we have

\[
(\dncast {\sigma} {\sigma'} \dncast {A_1} {A_2} M_2, \, M_3)
\in \gtierel {d_\sigma \circ d_\sigma'} {j} {\gtivrel {c \circ e} {}}.
\]

Then applying mixed transitivity, we have

\[
(M_1, M_3) \in \gtierel {d_\sigma \circ d_\sigma'} j {\gtivrel {c \circ e} {}},
\]

as desired.

M : σB(ϕ_E) = (σ) ∀∈σ.
x,k ϕ_E()[λo. E[k(o)]/k] ≡E[k(x)]

E[M] ≡M x E[x] ϕ_E

We show the left-to-right direction of the equivalence; the other direction is symmetric.
The proof is by Löb-induction. That is, we suppose that

\[
(E[M][\gamma_1], (\hndl M x {E[x]} \phi_E)[\gamma_2])
\in (\later^m \simierel {\sigma} {})_j {\simivrel {A} {}},
\]

for all $m$ and all $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$, and we show under this assumption that

\[
(E[M], \hndl M x {E[x]} \phi_E) \in \simierel {\sigma} {j} {\simivrel {A} {}}.
\]

Let $(\gamma_1, \gamma_2) \in \simigrel {\Gamma} {j}$.
We need to show that

\begin{align*}
( &E[M][\gamma_1],
(\hndl M x {E[x]} \phi_E )[\gamma_2] ) \\
&\quad\quad \in \simierel {\sigma} {j} {\simivrel {A} {}}.
\end{align*}

By Monadic Bind (Lemma <ref>),
and reflexivity, we have the following cases:

Let $k \le j$ and let $(V_1, V_2) \in \simivrel {B} {k}$.
We need to show that

\begin{align*}
( &E[V_1],
(\hndl {V_2} x {E[\gamma_2(x)]} {\phi_E} ) ) \\
&\quad\quad \in \simierel {\sigma} {j} {\simivrel {A} {}}.
\end{align*}

According to the operational semantics, the above handle term reduces to $(E[\gamma_2(x)])[V_2/x]$,
which is equal to $E[V_2]$.
By anti-reduction, it suffices to show that $(E[V_1], E[V_2]) \in \simierel {\sigma} {j} {\simivrel {A} {}}$,
but this follows from our assumption on $V_1$ and $V_2$ and the fact that they are passed
as input to the same evaluation context $E$.

We now show the third hypothesis of the lemma.
Let $k \le j$ and let $\effname$ be such that $E_1$ catches $\effname$ or $E_2$ catches $\effname$.
(Recall that $E_1 = E$ and $E_2 = \hndl \hole x {E[\gamma_2(x)]} \phi_E$.)
That is, $\effname @ c_i \leadsto d_i$ is in the domain of $\phi_E$.

Define $E_1 = E[\gamma_1]$ and $E_2 = E[\gamma_2]$.

Let $(V^l, V^r) \in (\later \simivrel {c_i} {})_k$, and let
$E^l \apart \effname$ and $E^r \apart \effname$ such that
$(x^l.E^l[x^l], x^r.E^r[x^r]) \in (\later \simikrel{d_i}{})_k
(\simierel{\sigma} {} {\simivrel {A} {}})$.

We need to show that

\begin{align*}
( &E[E^l[\raiseOpwithM{\effname}{V^l}]],
(\hndl {E^r[\raiseOpwithM{\effname}{V^r}]} x {E[x]} {\phi_E} ) ) \\
&\quad\quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

Since $E^r \apart \effname$, we have by the operational semantics that
the above handle term steps to

\[
\phi_E(\effname)[V^r/x][(\lambda o.\hndl {E^r[o]} x {E[x]} {\phi_E})/k].
\]

Thus, it will suffice by anti-reduction to show

\begin{align*}\label{handle_eta_2_goal}
( &E[E^l[\raiseOpwithM{\effname}{V^l}]],\,
\phi_E(\effname)[V^r/x][(\lambda o.\hndl {E^r[o]} {x} {E[x]} {\phi_E})/k]
) \\
&\quad\quad \in \simierel {\sigma} {k} {\simivrel {A} {}}.
\end{align*}

Let $\tilde{E} = \hndl \hole {x} {E[x]} {\phi_E}$, let
$k^l = \lambda s.E^l[s]$ and $k^r = \lambda s.E^r[s]$.

Using the premise, we have

\[
\tilde{E}[k^r(\raiseOpwithM{\effname}{V^r})],\,
\phi_{\tilde{E}}(\effname)[V^r/x][\lambda o. \tilde{E}[k^r(o)] /k]
) \in \simierel {\sigma} {\omega} {\simivrel {B} {}}.
\]

That is, we have

\begin{align*}
& \hndl {E^r(\raiseOpwithM{\effname}{V^r})} {x} {E[x]} {\phi_E}, \\