diff --git a/jfp-paper/defs.tex b/jfp-paper/defs.tex
index ab761f10810f794e482881a37af72b57f097a574..781407cd92a953852e3dcc36cb4b4820e9250f7a 100644
--- a/jfp-paper/defs.tex
+++ b/jfp-paper/defs.tex
@@ -161,6 +161,7 @@
 
 \newcommand\cbvtocbpvcomp[1]{#1^{c}}
 \newcommand\cbvtocbpvval[1]{#1^{v}}
+\newcommand\cbvtocbpvstk[1]{#1^{s}}
 \newcommand\cbvtocbpvty[1]{#1^{ty}}
 \newcommand\purely{\downarrow}
 
diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index b6826a7d7cf7bd736a48d8619499678c550e0911..0d59265e91c66971624156eb2b806064ed4cd12c 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -3952,7 +3952,7 @@ of the operational behavior of a standard Call-by-value cast calculus.
     {\dyn} \alt {A \to A} \alt {1}\alt {A \times A}\alt 0 \alt {A + A}\\
       \mbox{Tags} & G & \bnfdef & \dyn \to \dyn \alt 1 \alt \dyn \times \dyn \alt 0 \alt \dyn + \dyn\\
       \mbox{Terms} & M,N & \bnfdef &
-      \err \alt x \alt
+      \err \alt x \alt \letXbeYinZ M x N
       \obcast{A}{A}M\alt
       () \alt \pmpairWtoinZ M N\alt
       (M,N) \alt \pmpairWtoXYinZ M x y N\\
@@ -3962,10 +3962,10 @@ of the operational behavior of a standard Call-by-value cast calculus.
       \lambda x:A. M \alt M\,N\\
 
       \mbox{Values} & V & \bnfdef &
-      \obcast G \dyn V \alt \lambda x:A. M \alt () \alt (V,V) \alt \inl V \alt \inr V \\
+      \obcast \dyn G V \alt \lambda x:A. M \alt () \alt (V,V) \alt \inl V \alt \inr V \\
     \mbox{Evaluation Contexts} & S & \bnfdef &
-    \bullet \alt \obcast B A S\alt
-    (S,N)\alt (M, S) \alt \pmpairWtoXYinZ S x y N\\
+    \bullet \alt \obcast B A S\alt \letXbeYinZ S x N \alt
+    (S,N)\alt (V, S) \alt \pmpairWtoXYinZ S x y N\\
     &&\alt&
     \inl S \alt \inr S \alt \caseofXthenYelseZ S {x_1.N_1}{x_2.N_2}\alt
     S\,N\alt V\,S\\
@@ -3978,49 +3978,49 @@ of the operational behavior of a standard Call-by-value cast calculus.
 
 \begin{figure}
   \begin{mathpar}
-    E[\letXbeYinZ V x N] \step E[N[V/x]]\and
-    E[(\lambda x:A. M)\,V] \step E[M[V/x]]\and
-    E[\pmpairWtoinZ V N] \step E[N]\and
-    E[\pmpairWtoXYinZ {(V_1,V_2)} {x_1}{x_2} N] \step E[N[V_1/x_1][V_2/x_2]]\and
-    E[\caseofXthenYelseZ {\inl V}{x_1. N_1}{x_2. N_2}] \step E[N_1[V/x_1]]\and
-    E[\caseofXthenYelseZ {\inr V}{x_1. N_1}{x_2. N_2}] \step E[N_2[V/x_2]]\\\\
+    S[\letXbeYinZ V x N] \step S[N[V/x]]\and
+    S[(\lambda x:A. M)\,V] \step S[M[V/x]]\and
+    S[\pmpairWtoinZ V N] \step S[N]\and
+    S[\pmpairWtoXYinZ {(V_1,V_2)} {x_1}{x_2} N] \step S[N[V_1/x_1][V_2/x_2]]\and
+    S[\caseofXthenYelseZ {\inl V}{x_1. N_1}{x_2. N_2}] \step S[N_1[V/x_1]]\and
+    S[\caseofXthenYelseZ {\inr V}{x_1. N_1}{x_2. N_2}] \step S[N_2[V/x_2]]\\\\
     \inferrule
     {}
-    {\obcast{\dyn}{\dyn}V \step E[V]}\and
+    {S[\obcast{\dyn}{\dyn}V] \step S[V]}\and
     \inferrule
     {A \ltdyn G}
-    {E[\obcast \dyn A V] \step E[\obcast{\dyn}{G}\obcast{G}{A}V]}\and
+    {S[\obcast \dyn A V] \step S[\obcast{\dyn}{G}\obcast{G}{A}V]}\and
     \inferrule
     {A \ltdyn G}
-    {E[\obcast A \dyn V] \step E[\obcast A G \obcast G \dyn V]}\and
+    {S[\obcast A \dyn V] \step S[\obcast A G \obcast G \dyn V]}\and
     \inferrule
     {}
-    {E[\obcast G \dyn \obcast \dyn G V] \step E[V]}\and
+    {S[\obcast G \dyn \obcast \dyn G V] \step S[V]}\and
     \inferrule
     {G \neq G'}
-    {E[\obcast {G'} \dyn \obcast \dyn {G} ]}\and
+    {S[\obcast {G'} \dyn \obcast \dyn {G}] \step \err}\and
     \inferrule
     {A \ltdyn G_A \and B \ltdyn G_B \and G_A \neq G_B}
-    {E[\obcast B A V] \step \err}\and
+    {S[\obcast B A V] \step \err}\and
     \inferrule
     {}
-    {E[\obcast{A_1' \to A_2'}{A_1 \to A_2}V]\step
-     E[\lambda x:A_1'. \obcast{A_2'}{A_2}(V\,(\obcast{A_1}{A_1'}x))]}\and
+    {S[\obcast{A_1' \to A_2'}{A_1 \to A_2}V]\step
+     S[\lambda x:A_1'. \obcast{A_2'}{A_2}(V\,(\obcast{A_1}{A_1'}x))]}\and
     \inferrule
     {}
-    {E[\obcast 1 1 ()] \step E[()]}\and
+    {S[\obcast 1 1 ()] \step S[()]}\and
     \inferrule
     {}
-    {E[\obcast{A_1' \times A_2'}{A_1 \times A_2}(V_1,V_2)] \step
-     E[(\obcast{A_1'}{A_1}V_1,\obcast{A_2'}{A_2}V_2)]}\and
+    {S[\obcast{A_1' \times A_2'}{A_1 \times A_2}(V_1,V_2)] \step
+     S[(\obcast{A_1'}{A_1}V_1,\obcast{A_2'}{A_2}V_2)]}\and
     \inferrule
     {}
-    {E[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inl V)}]\step
-    E[\obcast{A_1'}{A_1}V]}\and
+    {S[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inl V)}]\step
+    S[\obcast{A_1'}{A_1}V]}\and
     \inferrule
     {}
-    {E[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inr V)}]\step
-    E[\obcast{A_2'}{A_2}V]}
+    {S[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inr V)}]\step
+    S[\obcast{A_2'}{A_2}V]}
   \end{mathpar}
   \caption{CBV Cast Calculus Operational Semantics}
 \end{figure}
@@ -4037,8 +4037,7 @@ of the operational behavior of a standard Call-by-value cast calculus.
     \cbvtocbpvcomp{(\letXbeYinZ M x N)} &=
     \bindXtoYinZ {\cbvtocbpvcomp{M}} x {\cbvtocbpvcomp{N}}\\
     \cbvtocbpvcomp{(\obcast{A_2}{A_1}M)} &=
-    \bindXtoYinZ M x
-    \dncast{F \cbvtocbpvty{A_2}}{F \dyn}{(\ret {\upcast{\cbvtocbpvty{A_1}}{\dyn}x})}\\
+    \dncast{F \cbvtocbpvty{A_2}}{F \dyn}\defupcast{F \cbvtocbpvty {A_1}}{F \dyn}[\cbvtocbpvcomp M]\\
     \cbvtocbpvcomp{(\lambda x:A. M)} &=
     \ret (\thunk {(\lambda x:\cbvtocbpvty{A}. \cbvtocbpvcomp{M})})\\
     \cbvtocbpvcomp{(M\,N)} &=
@@ -4046,8 +4045,8 @@ of the operational behavior of a standard Call-by-value cast calculus.
     \bindXtoYinZ {\cbvtocbpvcomp N} x
     \force f\,x\\
     \cbvtocbpvcomp{()} &= \ret ()\\
-    \cbvtocbpvcomp{(\pmpairWtoinZ M N)} &=
-    \bindXtoYinZ {\cbvtocbpvcomp M} z \pmpairWtoinZ z N\\
+    \cbvtocbpvcomp{(\pmpairWtoinZ S N)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp S} z \pmpairWtoinZ z {\cbvtocbpvcomp N}\\
     \cbvtocbpvcomp{(M_1,M_2)} &=
     \bindXtoYinZ {\cbvtocbpvcomp {M_1}} {x_1}
     \bindXtoYinZ {\cbvtocbpvcomp {M_2}} {x_2}
@@ -4070,11 +4069,310 @@ of the operational behavior of a standard Call-by-value cast calculus.
     \cbvtocbpvval{()} &= ()\\
     \cbvtocbpvval{(V_1,V_2)} &= (\cbvtocbpvval {V_1}, \cbvtocbpvval {V_2})\\
     \cbvtocbpvval{(\inl V)} &= \inl \cbvtocbpvval V \\
-    \cbvtocbpvval{(\inr V)} &= \inr \cbvtocbpvval V \\
+    \cbvtocbpvval{(\inr V)} &= \inr \cbvtocbpvval V \\\\
+    \cbvtocbpvstk{\bullet} &= \bullet\\
+    \cbvtocbpvstk{(\letXbeYinZ S x N)} &=
+    \bindXtoYinZ {\cbvtocbpvstk{S}} x {\cbvtocbpvcomp{N}}\\
+    \cbvtocbpvstk{(\obcast{A_2}{A_1}S)} &=
+    \bindXtoYinZ {\cbvtocbpvstk{S}} x
+    \dncast{F \cbvtocbpvty{A_2}}{F \dyn}{(\ret {\upcast{\cbvtocbpvty{A_1}}{\dyn}x})}\\
+    \cbvtocbpvstk{(S\,N)} &=
+    \bindXtoYinZ {\cbvtocbpvstk S} f
+    \bindXtoYinZ {\cbvtocbpvcomp N} x
+    \force f\,x\\
+    \cbvtocbpvstk{(V\,S)} &=
+    \bindXtoYinZ {\cbvtocbpvstk S} x
+    \force {\cbvtocbpvval V}\,x\\
+    \cbvtocbpvstk{(\pmpairWtoinZ S N)} &=
+    \bindXtoYinZ {\cbvtocbpvstk S} z \pmpairWtoinZ z {\cbvtocbpvcomp N}\\
+    \cbvtocbpvstk{(S_1,M_2)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp {S_1}} {x_1}
+    \bindXtoYinZ {\cbvtocbpvcomp {M_2}} {x_2}
+    \ret (x_1,x_2)\\
+    \cbvtocbpvstk{(V_1,S_2)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp {S_2}} {x_2}
+    \ret (\cbvtocbpvval{V_1},x_2)\\
+    \cbvtocbpvstk{(\pmpairWtoXYinZ S x y N)} &=
+    \bindXtoYinZ {\cbvtocbpvstk S} z
+    \pmpairWtoXYinZ z x y {\cbvtocbpvcomp N}\\
+    \cbvtocbpvstk{(\abort S)} &=
+    \bindXtoYinZ {\cbvtocbpvstk S} z {\abort z}\\
+    \cbvtocbpvstk{(\inl S)} &=
+    \bindXtoYinZ {\cbvtocbpvstk{S}} x \ret \inl x\\
+    \cbvtocbpvstk{(\inr S)} &=
+    \bindXtoYinZ {\cbvtocbpvstk{S}} x \ret \inr x\\
+    \cbvtocbpvstk{(\caseofXthenYelseZ S {x_1. N_1}{x_2. N_2})} &=
+    \bindXtoYinZ {\cbvtocbpvstk S} z
+    \caseofXthenYelseZ z {x_1. \cbvtocbpvcomp {N_1}}{x_2. \cbvtocbpvcomp {N_2}}\\\\
   \end{align*}
   \caption{CBV to GTT translation}
 \end{figure}
 
+\begin{lemma}
+  \label{lem:cbv-val-coh}
+  $\cbvtocbpvcomp V \equidyn \ret \cbvtocbpvval V$
+\end{lemma}
+\begin{proof}
+  By induction on $V$.
+  \begin{itemize}
+  \item $\obcast \dyn G V$:
+    \begin{align*}
+      \cbvtocbpvcomp{(\obcast G \dyn V)} &=
+      \bindXtoYinZ {\cbvtocbpvcomp V} x
+      \dncast{F \dyn}{F \dyn}{(\ret {\upcast{\cbvtocbpvty G}{\dyn}x})}\tag{definition}\\
+      &\equidyn 
+      \bindXtoYinZ {\ret \cbvtocbpvval V} x
+      \dncast{F \dyn}{F \dyn}{(\ret {\upcast{\cbvtocbpvty G}{\dyn}x})}\tag{I.H.}\\
+      &\equidyn 
+      \dncast{F \dyn}{F \dyn}{(\ret {\upcast{\cbvtocbpvty G}{\dyn}\cbvtocbpvval V})}\tag{$F\beta$}\\
+      &\equidyn 
+      {\ret {\upcast{\cbvtocbpvty G}{\dyn}\cbvtocbpvval V}}\tag{Theorem \ref{thm:decomposition}}\\
+    \end{align*}
+  \item $\lambda x:A. M$: immediate by reflexivity.
+  \item $()$: immediate by reflexivity.
+  \item $(V_1,V_2)$:
+    \begin{align*}
+      \cbvtocbpvcomp{(V_1,V_2)} &=
+      \bindXtoYinZ {\cbvtocbpvcomp {V_1}} {x_1}
+      \bindXtoYinZ {\cbvtocbpvcomp {V_2}} {x_2}
+      \ret (x_1,x_2)\tag{definition}\\
+      &\equidyn
+      \bindXtoYinZ {\ret\cbvtocbpvval {V_1}} {x_1}
+      \bindXtoYinZ {\ret\cbvtocbpvval {V_2}} {x_2}
+      \ret (x_1,x_2)\tag{I.H., twice}\\
+      &\equidyn \ret (V_1,V_2)\tag{$F\beta$ twice}
+    \end{align*}
+  \item $\inl V$:
+    \begin{align*}
+    \cbvtocbpvcomp{(\inl V)} &=
+    \bindXtoYinZ {\cbvtocbpvcomp{V}} x \ret \inl x\tag{definition}\\
+    &\equidyn \bindXtoYinZ {\ret\cbvtocbpvval{V}} x \ret \inl x\tag{I.H.}\\
+    &\equidyn \ret\inl \cbvtocbpvval{V} \tag{$F\beta$}
+    \end{align*}
+  \item $\inr V$: similar to $\inl$ case.
+  \end{itemize}
+\end{proof}
+
+\begin{lemma}
+  \label{lem:cbpv-subst}
+  $\cbvtocbpvcomp{(M[V/x])} \equidyn \cbvtocbpvcomp{M} [ \cbvtocbpvval V / x]$
+\end{lemma}
+\begin{proof}
+  By induction on $M$. All cases but variable are by congruence and
+  inductive hypothesis.
+  \begin{itemize}
+  \item $M = x$:
+    \begin{align*}
+      \cbvtocbpvcomp{(x[V/x])} &= \cbvtocbpvcomp{V} \tag{def. substitution}\\
+      &\equidyn \ret \cbvtocbpvval{V} \tag{Lemma \ref{lem:cbv-val-coh}}\\
+      &= (\ret x)[\cbvtocbpvval{V}/x]\tag{def. substitution}\\
+      &= (\cbvtocbpvcomp{x})[\cbvtocbpvval{V}/x]\tag{def. substitution}\\
+    \end{align*}
+  \item $M = y \neq x$:
+    \begin{align*}
+      \cbvtocbpvcomp{(y[V/x])} &= \cbvtocbpvcomp{y} \tag{def. subst.}\\
+      &\equidyn \ret y \tag{def.}\\
+      &\equidyn (\ret y)[V/x] \tag{def. subst.}
+    \end{align*}
+  \end{itemize}
+\end{proof}
+
+\begin{lemma}
+  \label{lem:cbv-evctxt-plug}
+  $\cbvtocbpvcomp{(S[M])} \equidyn \cbvtocbpvstk{S}[\cbvtocbpvcomp{M}]$
+\end{lemma}
+\begin{proof}
+  By induction on $S$. Most cases are straightforward by congruence
+  and induction hypothesis. We show the other cases.
+  \begin{itemize}
+  \item $S = V\,S$:
+    \begin{align*}
+      \cbvtocbpvcomp{((V\,S)[M])} &= \cbvtocbpvcomp{(V\,(S[M]))} \tag{defn. plugging} \\
+      &= \bindXtoYinZ {\cbvtocbpvcomp V} f
+      \bindXtoYinZ {\cbvtocbpvcomp {(S[M])}} x
+      \force f\,x \tag{defn.}\\
+      &\equidyn
+      \bindXtoYinZ {\ret\cbvtocbpvval V} f
+      \bindXtoYinZ {\cbvtocbpvcomp {(S[M])}} x
+      \force f\,x\tag{Lemma \ref{lem:cbv-val-coh}}\\
+      &\equidyn
+      \bindXtoYinZ {\cbvtocbpvcomp {(S[M])}} x
+      \force {\cbvtocbpvval V}\,x\tag{$F\beta$}\\
+      &\equidyn
+      \bindXtoYinZ {\cbvtocbpvstk S [\cbvtocbpvcomp M]} x
+      \force {\cbvtocbpvval V}\,x\tag{I.H.}\\
+      &\equidyn
+      (\bindXtoYinZ {\cbvtocbpvstk S} x \force {\cbvtocbpvval V}\,x)[\cbvtocbpvcomp M] \tag{defn. of plug}\\
+      &= \cbvtocbpvstk{(V\,S)}[\cbvtocbpvcomp M]
+    \end{align*}
+  \item $S = (V_1,S_2)$
+    \begin{align*}
+      \cbvtocbpvcomp{((V_1,S_2)[M])} &= \cbvtocbpvcomp{(V_1,S_2[M])} \tag{defn. plugging} \\
+      &=
+      \bindXtoYinZ {\cbvtocbpvcomp {V_1}} {x_1}
+      \bindXtoYinZ {\cbvtocbpvcomp {S_2[M]}} {x_2}
+      \ret (x_1,x_2)\tag{defn.}\\
+      &\equidyn
+      \bindXtoYinZ {\ret\cbvtocbpvval {V_1}} {x_1}
+      \bindXtoYinZ {\cbvtocbpvcomp {S_2[M]}} {x_2}
+      \ret (x_1,x_2)\tag{Lemma \ref{lem:cbv-val-coh}}\\
+      &\equidyn
+      \bindXtoYinZ {\cbvtocbpvcomp {S_2[M]}} {x_2}
+      \ret (\cbvtocbpvval {V_1},x_2)\tag{$F\beta$}\\
+      &\equidyn
+      \bindXtoYinZ {\cbvtocbpvstk {S_2}[\cbvtocbpvcomp M]} {x_2}
+      \ret (\cbvtocbpvval {V_1},x_2)\tag{I.H.}\\
+      &=
+      (\bindXtoYinZ {\cbvtocbpvstk {S_2}} {x_2} \ret (\cbvtocbpvval {V_1},x_2))[\cbvtocbpvcomp M]\tag{defn. plugging}\\
+      &= (V_1,\cbvtocbpvstk{S_2})[\cbvtocbpvcomp M]\tag{defn.}\\
+    \end{align*}
+  \end{itemize}
+\end{proof}
+
+\begin{lemma}[Any Middle Type will Do]
+  \label{lem:cbv-upcast-downcast}
+  If $A_1,A_2 \ltdyn A'$, then
+  $\dncast{F A_2}{F \dyn}\defupcast{F A_1}{F \dyn}M \equidyn \dncast{F A_2}{F A'}\defupcast{F A_1}{F A'}M$
+\end{lemma}
+\begin{proof}
+  \begin{align*}
+    \dncast{F A_2}{F \dyn}\defupcast{F A_1}{F \dyn}M
+    &\equidyn \dncast{F A_2}{F A'}\dncast{F A'}{F \dyn}\defupcast{F A'}{F \dyn}\defupcast{F A_1}{F A'}M\tag{Theorem\ref{thm:decomposition}}\\
+    &\equidyn \dncast{F A_2}{F A'}\defupcast{F A_1}{F A'}M\tag{retraction}\\
+  \end{align*}
+\end{proof}
+
+\begin{theorem}
+  If $M \step N$ then $\cbvtocbpvcomp M \equidyn \cbvtocbpvcomp N$.
+\end{theorem}
+\begin{proof}
+  In all cases, by Lemma \ref{lem:cbv-evctxt-plug}, congruence and
+  $S[\err]\equidyn \err$, it is sufficient to consider the case that
+  $S = \bullet$.
+
+  First, we have the cases not involving casts, which are standard for
+  the embedding of call-by-value into call-by-push-value.
+  \begin{itemize}
+  \item TODO
+  \end{itemize}
+  Next, we have the interesting cases, those specific to gradual type
+  casts/GTT.
+  \begin{itemize}
+  \item ${\obcast{\dyn}{\dyn}V \step V}$:
+    \begin{align*}
+      \cbvtocbpvcomp{(\obcast{\dyn}{\dyn}V)} &=
+      \dncast{F \dyn}{F \dyn}\defupcast{F \dyn}{F \dyn}[\cbvtocbpvcomp V]\\
+      &\equidyn {{{\cbvtocbpvcomp V}}}\tag{Theorem\ref{decomposition}}\\
+    \end{align*}
+  \item $\obcast \dyn A V \step \obcast{\dyn}{G}\obcast{G}{A}V$ where
+    $A \ltdyn G$
+    \begin{align*}
+      \cbvtocbpvcomp{\obcast \dyn A V} &\equidyn
+      \dncast{F \dyn}{F \dyn}\defupcast{F \cbvtocbpvty{A}}{F \dyn}[\cbvtocbpvcomp V]\\
+      &\equidyn
+      \defupcast{F \cbvtocbpvty{A}}{F \dyn}[\cbvtocbpvcomp V]\tag{Theorem\ref{thm:decomposition}}\\
+      &\equidyn
+      \defupcast{F \cbvtocbpvty{G}}{F \dyn}\defupcast{F \cbvtocbpvty{A}}{F \cbvtocbpvty{G}}[\cbvtocbpvcomp V]\tag{Theorem\ref{thm:decomposition}}\\
+    \end{align*}
+  \item $\obcast A \dyn V \step \obcast A G \obcast G \dyn V$: similar to previous case.
+  \item $\obcast G \dyn \obcast \dyn G V \step V$
+    \begin{align*}
+      \cbvtocbpvcomp{(\obcast G \dyn \obcast \dyn G V)}
+      &= \dncast{F \cbvtocbpvty G}{F \dyn}\defupcast{F \dyn}{F \dyn}\dncast{F \dyn}{F \dyn}\defupcast{F \cbvtocbpvty G}{F \dyn}[\cbvtocbpvcomp V]\\
+      &\equidyn
+      \dncast{F \cbvtocbpvty G}{F \dyn}\defupcast{F \cbvtocbpvty G}{F \dyn}[\cbvtocbpvcomp V]\tag{Theorem\ref{thm:decomposition}}\\   
+      &\equidyn \cbvtocbpvcomp V\tag{retraction}\\   
+    \end{align*}
+  \item $\obcast{A_1' \to A_2'}{A_1 \to A_2}V \step \lambda x:A_1'. \obcast{A_2'}{A_2}(V\,(\obcast{A_1}{A_1'}x))$
+    \begin{align*}
+      &\cbvtocbpvcomp{(\obcast{A_1' \to A_2'}{A_1 \to A_2}V)}\\
+      &\equidyn
+      \dncast{FU(\cbvtocbpvty{A_1'} \to F\cbvtocbpvty{A_2'})}{F\dyn}\defupcast{FU(\cbvtocbpvty{A_1} \to F\cbvtocbpvty{A_2})}{F\dyn}\cbvtocbpvcomp{V}\\
+      &\equidyn
+      \dncast{FU(\cbvtocbpvty{A_1'} \to F\cbvtocbpvty{A_2'})}{FU(\dyn \to F \dyn)}\defupcast{FU(\cbvtocbpvty{A_1} \to F\cbvtocbpvty{A_2})}{FU(\dyn \to F \dyn)}\cbvtocbpvcomp{V}\\
+      &\equidyn
+      \dncast{FU(\cbvtocbpvty{A_1'} \to F\cbvtocbpvty{A_2'})}{FU(\dyn \to F \dyn)}\defupcast{FU(\cbvtocbpvty{A_1} \to F\cbvtocbpvty{A_2})}{FU(\dyn \to F \dyn)}[\ret\cbvtocbpvval{V}]\\
+      &\equidyn
+      \dncast{FU(\cbvtocbpvty{A_1'} \to F\cbvtocbpvty{A_2'})}{FU(\dyn \to F \dyn)}\ret\upcast{U(\cbvtocbpvty{A_1} \to F\cbvtocbpvty{A_2})}{U(\dyn \to F \dyn)}\cbvtocbpvval{V}\\
+      &\equidyn
+      \dncast{FU(\cbvtocbpvty{A_1'} \to F\cbvtocbpvty{A_2'})}{FU(\dyn \to F \dyn)}\\
+      &\qquad\ret\thunk {(\lambda x'.
+        \bindXtoYinZ{\dncast{\u F {\cbvtocbpvty {A_1}}}{\u F \dyn}{(\ret x')}}{x}{}{\force{(\upcast{U \u F {\cbvtocbpvty {A_2}}}{U \u F \dyn}{(\thunk{(\force{\cbvtocbpvval V}\,x)})})}} )}\\
+      &\equidyn
+      \dncast{FU(\cbvtocbpvty{A_1'} \to F\cbvtocbpvty{A_2'})}{FU(\dyn \to F \dyn)}\\
+      &\qquad\ret\thunk {(\lambda x'.
+        \bindXtoYinZ{\dncast{\u F {\cbvtocbpvty {A_1}}}{\u F \dyn}{(\ret x')}}{x}{}{\defupcast{\u F {\cbvtocbpvty {A_2}}}{\u F \dyn}(\force{\cbvtocbpvval V}\,x)} )}\\
+      &\equidyn
+      \ret\thunk {(\dncast{\cbvtocbpvty{A_1'} \to F\cbvtocbpvty{A_2'}}{\dyn \to F \dyn} {(\lambda x'.
+        \bindXtoYinZ{\dncast{\u F {\cbvtocbpvty {A_1}}}{\u F \dyn}{(\ret x')}}{x}{}{\defupcast{\u F {\cbvtocbpvty {A_2}}}{\u F \dyn}(\force{\cbvtocbpvval V}\,x)} )})}\\
+      &\equidyn
+      \ret\thunk{(
+      \lambda y'.
+      \dncast{\u F\cbvtocbpvty{A_2'}}{\u F \dyn}
+      {({(\lambda x'.
+        \bindXtoYinZ{\dncast{\u F {\cbvtocbpvty {A_1}}}{\u F \dyn}{(\ret x')}}{x}{}{\defupcast{\u F {\cbvtocbpvty {A_2}}}{\u F \dyn}(\force{\cbvtocbpvval V}\,x)} )})\,(\upcast{\cbvtocbpvty{A_1'}}{\dyn}{y'})})} \\
+      &\equidyn
+      \ret\thunk{(
+      \lambda y'.
+      \dncast{\u F\cbvtocbpvty{A_2'}}{\u F \dyn}
+      {({(
+        \bindXtoYinZ{\dncast{\u F {\cbvtocbpvty {A_1}}}{\u F \dyn}{(\ret (\upcast{\cbvtocbpvty{A_1'}}{\dyn}{y'})}}{x}{}{\defupcast{\u F {\cbvtocbpvty {A_2}}}{\u F \dyn}(\force{\cbvtocbpvval V}\,x)} )})})} \\
+      &\equidyn
+      \ret\thunk{(
+      \lambda y'.
+      \dncast{\u F\cbvtocbpvty{A_2'}}{\u F \dyn}
+      {({(
+        \bindXtoYinZ{\dncast{\u F {\cbvtocbpvty {A_1}}}{\u F \dyn}{\defupcast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}{\ret y'}}}{x}{}{\defupcast{\u F {\cbvtocbpvty {A_2}}}{\u F \dyn}(\force{\cbvtocbpvval V}\,x)} )})})} \\
+      &\equidyn
+      \ret\thunk{(
+      \lambda y'.
+      \dncast{\u F\cbvtocbpvty{A_2'}}{\u F \dyn}
+      {({(
+        \bindXtoYinZ{\cbvtocbpvty{(\obcast{A_1}{A_1'}y')}}{x}{\defupcast{\u F {\cbvtocbpvty {A_2}}}{\u F \dyn}(\force{\cbvtocbpvval V}\,x)})})})} \\
+      &\equidyn
+      \ret\thunk{(
+      \lambda y'.
+      \dncast{\u F\cbvtocbpvty{A_2'}}{\u F \dyn}\defupcast{\u F {\cbvtocbpvty {A_2}}}{\u F \dyn}{(
+      \bindXtoYinZ{\cbvtocbpvty{(\obcast{A_1}{A_1'}y')}}{x}
+      (\force{\cbvtocbpvval V}\,x))})} \\
+      &\equidyn
+      \ret\thunk{(
+      \lambda y'.
+      \dncast{\u F\cbvtocbpvty{A_2'}}{\u F \dyn}\defupcast{\u F {\cbvtocbpvty {A_1}}}{\u F \dyn}{(
+      \bindXtoYinZ{\cbvtocbpvcomp{V}}{f}
+      \bindXtoYinZ{\cbvtocbpvcomp{(\obcast{A_1}{A_1'}y')}}{x}
+      (\force f\,x))})} \\
+      &\equidyn
+      \ret\thunk{(
+      \lambda y'.
+      \dncast{\u F\cbvtocbpvty{A_2'}}{\u F \dyn}\defupcast{\u F {\cbvtocbpvty {A_1}}}{\u F \dyn}{\cbvtocbpvcomp{(V\,(\obcast{A_1}{A_1 '}y'))}})} \\
+      &\equidyn
+      \ret\thunk{(
+      \lambda y'.
+      {\cbvtocbpvcomp{(\obcast{A_2'}{A_2}(V\,(\obcast{A_1}{A_1'}y')))}})} \\
+      &\equidyn
+      \cbvtocbpvcomp{(\lambda y'. \obcast{A_2'}{A_2}(V\,(\obcast{A_1}{A_1'}y')))}
+    \end{align*}
+  \end{itemize}
+  \begin{mathpar}
+    \inferrule
+    {}
+    {S[\obcast 1 1 ()] \step S[()]}\and
+    \inferrule
+    {}
+    {S[\obcast{A_1' \times A_2'}{A_1 \times A_2}(V_1,V_2)] \step
+     S[(\obcast{A_1'}{A_1}V_1,\obcast{A_2'}{A_2}V_2)]}\and
+    \inferrule
+    {}
+    {S[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inl V)}]\step
+    S[\obcast{A_1'}{A_1}V]}\and
+    \inferrule
+    {}
+    {S[\obcast{A_1' + A_2'}{A_1 + A_2}{(\inr V)}]\step
+    S[\obcast{A_2'}{A_2}V]}
+  \end{mathpar}
+\end{proof}
+
 
 \section{Contract Models of GTT}
 \label{sec:contract}