\Gamma, x : A_1,y : A_2\vDash M \logpole M' \in\u B
}
{\Gamma\vDash\pmpairWtoXYinZ V x y M \logpole\pmpairWtoXYinZ{V'}{x}{y}{M'}\in\u B}$
By $V \logty i {A_1\times A_2} V'$, we know $V[\gamma_1]=
(V_1,V_2)$ and $V'[\gamma_2]=(V_1', V_2')$ with $V_1\logty i
{A_1} V_1'$ and $V_2\logty i {A_2} V_2'$.
Then by anti-reduction, the problem reduces to
\[ S_1[M[\gamma_1,V_1/x,V_2/y]]\ipole i S_1[M'[\gamma_1,V_1'/x,V_2'/y]]\]
which follows by assumption.
\item$\inferrule
{\Gamma\vDash V \logpole V' \in A[\mu X.A/X]}
{\Gamma\vDash\rollty{\mu X.A} V \logpole\rollty{\mu X.A} V' \in\mu X.A }$
If $i =0$, we're done. Otherwise $i=j+1$, and our assumption is
that $V[\gamma_1]\logty{j+1} V'[\gamma_2]$ and we need to show
that $\roll V[\gamma_1]\logty{j+1}{\mu X. A}\roll
V'[\gamma_2]$. By definition, we need to show $V[\gamma_1]\logty
j V'[\gamma_2]$, which follows by downward-closure.
\item$\inferrule
{\Gamma\vDash V \logpole V' \in\mu X. A\and
\Gamma, x : A[\mu X. A/X]\vDash M \logpole M' \in\u B}
{\Gamma\vDash\pmmuXtoYinZ V x M \logpole\pmmuXtoYinZ{V'}{x}{M'}\in\u B}$
If $i =0$, then by triviality at $0$, we're done.
Otherwise, $V[\gamma_1]\logty{j+1}{\mu X. A} V'[\gamma_2]$ so
$V[\gamma_1]=\roll V_\mu, V'[\gamma_2]=\roll V_\mu'$ with
$V_\mu\logty j {A[\mu X.A/X]} V_\mu'$. Then each side takes $1$ step, so by anti-reduction it is sufficient to show
\[ S_1[M[\gamma_1,V_\mu/x]]\ipole j S_2[M'[\gamma_2,V_\mu'/x]]\] which follows by assumption and downward closure of the stack, value relations.
\item$\inferrule{\Gamma\vDash M \logpole M' \in\u B}{\Gamma
\vDash\thunk M \logpole\thunk M' \in U \u B}$. We need to show
$M[\gamma_1]\logty i {U \u B} M'[\gamma_2]$, so let $S_1\logty
j {\u B} S_2$. Then by downward-closure $\gamma_1\logty j
{\Gamma}\gamma_2$, so by assumption, $S_1[M_1[\gamma_1]]\ipole
j S_2[M_2[\gamma_2]]$.
\item$\inferrule
{\Gamma\vDash V \logpole V' \in U \u B}
{\Gamma\vDash\force V \logpole\force V' \in\u B}$.
We need to show $S_1[\force V[\gamma_1]]\ipole i S_2[\force
V'[\gamma_2]]$, which follows by the orthogonality definition of
$V[\gamma_1]\logty i {U \u B} V'[\gamma_2]$.
\item$\inferrule
{\Gamma\vDash V \logpole V' \in A}
{\Gamma\vDash\ret V \logpole\ret V' \in\u F A}$
We need to show $S_1[\ret V[\gamma_1]]\ipole i S_2[\ret
V'[\gamma_2]]$, which follows by the orthogonality definition of
$S_1\logty i {\u F A} S_2$.
\item$\inferrule
{\Gamma\vDash M \logpole M' \in\u F A\and
\Gamma, x: A \vDash N \logpole N' \in\u B}
{\Gamma\vDash\bindXtoYinZ M x N \logpole\bindXtoYinZ{M'}{x}{N'}\in\u B}$.
We need to show $\bindXtoYinZ{M[\gamma_1]} x {N[\gamma_2]}\ipole i \bindXtoYinZ{M'[\gamma_2]}{x}{N'[\gamma_2]}$.
By $M \logpole M' \in\u F A$, it is sufficient to show that
\[\bindXtoYinZ\bullet x {N[\gamma_1]}\logty i {\u F A}\bindXtoYinZ\bullet{x}{N'[\gamma_2]}\]
So let $j \leq i$ and $V \logty j A V'$, then we need to show
\[\bindXtoYinZ{\ret V} x {N[\gamma_1]}\logty j {\u F A}\bindXtoYinZ{\ret V'}{x}{N'[\gamma_2]}\]
By anti-reduction, it is sufficient to show
\[ N[\gamma_1,V/x]\ipole j N'[\gamma_2,V'/x]\]
which follows by anti-reduction for $\gamma_1\logty i {\Gamma}\gamma_2$ and $N \logpole N'$.
\item$\inferrule
{\Gamma, x: A \vDash M \logpole M' \in\u B}
{\Gamma\vDash\lambda x : A . M \logpole\lambda x:A. M' \in A \to\u B}$
We need to show $S_1[\lambda x:A. M[\gamma_1]]\ipole i S_2[\lambda x:A.M'[\gamma_2]]$.
By $S_1\logty i {A \to\u B} S_2$, we know $S_1= S_1'[\bullet V_1]$, $S_2= S_2'[\bullet V_2]$ with $S_1' \logty i {\u B} S_2'$ and $V_1\logty i {A} V_2$.
Then by anti-reduction it is sufficient to show
\[
S_1'[M[\gamma_1,V_1/x]]\ipole i S_2'[M'[\gamma_2,V_2/x]]
\]
which follows by $M \logpole M'$.
\item$\inferrule
{\Gamma\vDash M \logpole M' \in A \to\u B\and
\Gamma\vDash V \logpole V' \in A}
{\Gamma\vDash M\,V \logpole M'\,V' \in\u B }$
We need to show $S_1[M[\gamma_1]\,V[\gamma_1]]\ipole i S_2[M'[\gamma_2]\,V'[\gamma_2]]$ so by $M \logpole M'$ it is sufficient to show $S_1[\bullet V[\gamma_1]]\logty i {A \to\u B} S_2[\bullet V'[\gamma_2]]$ which follows by definition and assumption that $V \logpole V'$.
We need to show $S_1[\pair{M_1[\gamma_1]}{M_2[\gamma_1]}]\ipole i S_2[\pair{M_1'[\gamma_1]}{M_2'[\gamma_2]}]$.
We proceed by case analsysis of $S_1\logty i {\u B_1\with\u B_2} S_2$
\begin{enumerate}
\item In the first possibility $S_1= S_{1}'[\pi\bullet], S_2=
S_2'[\pi\bullet]$ and $S_1' \logty i {\u B_1} S_2'$.
Then by anti-reduction, it is sufficient to show
\[ S_1'[M_1[\gamma_1]]\ipole i S_2'[M_1'[\gamma_2]]\]
which follows by $M_1\logpole M_1'$.
\item Same as previous case.
\end{enumerate}
\item$\inferrule
{\Gamma\vDash M \logpole M' \in\u B_1\with\u B_2}
{\Gamma\vDash\pi M \logpole\pi M' \in\u B_1}$
We need to show $S_1[\pi M[\gamma_1]]\ipole i S_2[\pi
M'[\gamma_2]]$, which follows by $S_1[\pi\bullet]\logty i {\u
B_1\with\u B_2} S_2[\pi\bullet]$ and $M \logpole M'$.
\item$\inferrule{\Gamma\vDash M \logpole M' \in\u B_1\with\u
B_2}{\Gamma\vDash\pi' M \logpole\pi' M' \in\u B_2}$ Similar
to previous case.
\item$\inferrule
{\Gamma\vDash M \logpole M' \in\u B[{\nu\u Y. \u B}/\u Y]}
{\Gamma\vDash\rollty{\nu\u Y. \u B} M \logpole\rollty{\nu\u Y. \u B} M' \in{\nu\u Y. \u B}}$
We need to show that
\[ S_1[\rollty{\nu\u Y. \u B} M[\gamma_1]]
\ipole i S_2[\rollty{\nu\u Y. \u B} M'[\gamma_2]]\]
If $i =0$, we invoke triviality at $0$.
Otherwise, $i = j +1$ and we know by $S_1\logty{j+1}{\nu\u Y. \u B} S_2$ that
$S_1= S_1'[\unroll\bullet]$ and $S_2= S_2'[\unroll\bullet]$ with $S_1' \logty j {\u B[{\nu\u Y. \u B}/\u Y]} S_2'$, so by anti-reduction it is sufficient to show
\[ S_1'[ M[\gamma_1]]\ipole i S_2'[ M'[\gamma_2]]\]
which follows by $M \logpole M'$ and downward-closure.
\item$\inferrule
{\Gamma\vDash M \logpole M' \in{\nu\u Y. \u B}}
{\Gamma\vDash\unroll M \logpole\unroll M' \in\u B[{\nu\u Y. \u B}/\u Y]}$
We need to show $S_1[\unroll M]\ipole i S_2[\unroll M']$, which
follows because $S_1[\unroll\bullet]\logty i {\nu\u Y. \u B}
S_2[\unroll\bullet]$ and $M \logpole M'$.
\end{enumerate}
\end{proof}
\begin{theorem}[Completeness of Logical wrt Contextual]
For any pole $\pole$, the logical lifting is complete with respect
to the contextual lifting.
\end{theorem}
\begin{proof}
TODO: modify the proof below
\end{proof}
\begin{theorem}[LR is Sound for Contextual Error Approximation]
\begin{enumerate}
\item If $\Gamma\vDash M_1\ltdyn M_2\in\u B$, then $\Gamma\vDash M_1\ltctx M_2\in\u B$.
