diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index 0d59265e91c66971624156eb2b806064ed4cd12c..bb682ea7f5048b5b02f724c1b4b902b8ab9f20a7 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -3980,7 +3980,7 @@ of the operational behavior of a standard Call-by-value cast calculus.
   \begin{mathpar}
     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[\pmpairWtoinZ () 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]]\\\\
@@ -4253,7 +4253,55 @@ of the operational behavior of a standard Call-by-value cast calculus.
   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
+  \item $\letXbeYinZ V x N \step N[V/x]$
+    \begin{align*}
+      \cbvtocbpvcomp{(\letXbeYinZ V x N)}
+      &= \bindXtoYinZ {\cbvtocbpvcomp V} x {\cbvtocbpvcomp N}\\
+      &\equidyn \bindXtoYinZ {\ret\cbvtocbpvval V} x {\cbvtocbpvcomp N}\\
+      &\equidyn {\cbvtocbpvcomp N}[{\cbvtocbpvval V}/x]\\
+      &\equidyn {\cbvtocbpvcomp {(N[V/x]})}
+    \end{align*}
+  \item $(\lambda x:A. M)\,V \step M[V/x]$
+    \begin{align*}
+      \cbvtocbpvcomp{((\lambda x:A. M)\,V)}
+      &= \bindXtoYinZ {(\ret (\thunk (\lambda x:\cbvtocbpvty A. \cbvtocbpvcomp M)))} f
+      \bindXtoYinZ {\cbvtocbpvcomp V} x
+      \force f \, x\\
+      &\equidyn \bindXtoYinZ {\cbvtocbpvcomp V} x
+      \force (\thunk (\lambda x:\cbvtocbpvty A. \cbvtocbpvcomp M)) \, x\\
+      &\equidyn \bindXtoYinZ {\ret \cbvtocbpvval V} x
+      \force (\thunk (\lambda x:\cbvtocbpvty A. \cbvtocbpvcomp M)) \, x\\
+      &\equidyn \force (\thunk (\lambda x:\cbvtocbpvty A. \cbvtocbpvcomp M)) \,\cbvtocbpvval V\\
+      &\equidyn (\lambda x:\cbvtocbpvty A. \cbvtocbpvcomp M)\,\cbvtocbpvval V\\
+      &\equidyn \cbvtocbpvcomp M[\cbvtocbpvval V/x]\\
+      &\equidyn \cbvtocbpvcomp {(M[V/x])}
+    \end{align*}
+  \item $\pmpairWtoinZ {()} N \step N$
+    \begin{align*}
+      \cbvtocbpvcomp{(\pmpairWtoinZ {()} N)}
+      &= \bindXtoYinZ {\ret ()} z \pmpairWtoinZ z \cbvtocbpvcomp N\\
+      &= \pmpairWtoinZ {()} \cbvtocbpvcomp N\\
+      &= \cbvtocbpvcomp N
+    \end{align*}
+  \item $\pmpairWtoXYinZ {(V_1,V_2)} {x_1}{x_2} N \step N[V_1/x_1][V_2/x_2]$
+    \begin{align*}
+      \cbvtocbpvcomp{(\pmpairWtoXYinZ {(V_1,V_2)} {x_1}{x_2} N)}
+      &= \bindXtoYinZ {\cbvtocbpvcomp{(V_1,V_2)}} z \pmpairWtoXYinZ z {x_1}{x_2} \cbvtocbpvcomp N\\
+      &\equidyn \bindXtoYinZ {\ret{(\cbvtocbpvval {V_1}, \cbvtocbpvval {V_2})}} z \pmpairWtoXYinZ z {x_1}{x_2} \cbvtocbpvcomp N\\
+      &\equidyn \pmpairWtoXYinZ {(\cbvtocbpvval {V_1}, \cbvtocbpvval {V_2})} {x_1}{x_2} \cbvtocbpvcomp N\\
+      &\equidyn {\cbvtocbpvcomp N}[\cbvtocbpvval {V_1}/x_1][\cbvtocbpvval {V_2}/x_2]\\
+      &\equidyn \cbvtocbpvcomp {(N[V_1/x_1][V_2/x_2])}
+    \end{align*}
+  \item $\caseofXthenYelseZ {\inl V}{x_1. N_1}{x_2. N_2} \step N_1[V/x_1]$
+    \begin{align*}
+      \cbvtocbpvcomp{(\caseofXthenYelseZ {\inl V}{x_1. N_1}{x_2. N_2})}
+      &= \bindXtoYinZ {\cbvtocbpvcomp{({\inl V})}} z \caseofXthenYelseZ z {x_1. \cbvtocbpvcomp N_1}{x_2. \cbvtocbpvcomp N_2}\\
+      &\equidyn \bindXtoYinZ {\ret(\inl \cbvtocbpvval V)} z \caseofXthenYelseZ z {x_1. \cbvtocbpvcomp N_1}{x_2. \cbvtocbpvcomp N_2}\\
+      &\equidyn \caseofXthenYelseZ {\inl \cbvtocbpvval V} {x_1. \cbvtocbpvcomp N_1}{x_2. \cbvtocbpvcomp N_2}\\
+      &\equidyn {\cbvtocbpvcomp N_1}[\cbvtocbpvval V/x_1]\\
+      &\equidyn {\cbvtocbpvcomp {(N_1[V/x_1])}}
+    \end{align*}
+  \item $\caseofXthenYelseZ {\inr V}{x_1. N_1}{x_2. N_2} \step N_2[V/x_2]$
   \end{itemize}
   Next, we have the interesting cases, those specific to gradual type
   casts/GTT.
@@ -4353,24 +4401,85 @@ of the operational behavior of a standard Call-by-value cast calculus.
       &\equidyn
       \cbvtocbpvcomp{(\lambda y'. \obcast{A_2'}{A_2}(V\,(\obcast{A_1}{A_1'}y')))}
     \end{align*}
+  \item $\obcast 1 1 () \step ()$
+    \begin{align*}
+      \cbvtocbpvcomp{(\obcast 1 1 ())}
+      &=
+      \dncast{\u F 1}{\u F \dyn}\defupcast{\u F 1}{\u F \dyn}[\ret ()]\\
+      &\equidyn \ret ()\\
+      &= \cbvtocbpvcomp{()}
+    \end{align*}
+  \item $\obcast{A_1' \times A_2'}{A_1 \times A_2}(V_1,V_2) \step (\obcast{A_1'}{A_1}V_1,\obcast{A_2'}{A_2}V_2)$
+    \begin{align*}
+      &\cbvtocbpvcomp{(\obcast{A_1' \times A_2'}{A_1 \times A_2}(V_1,V_2))}\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} \times \cbvtocbpvty{A_2'})}{\u F \dyn}\defupcast{\u F (\cbvtocbpvty{A_1} \times \cbvtocbpvty{A_2})}{\u F \dyn}\cbvtocbpvcomp{(V_1,V_2)}\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} \times \cbvtocbpvty{A_2'})}{\u F (\dyn\times\dyn)}\defupcast{\u F (\cbvtocbpvty{A_1} \times \cbvtocbpvty{A_2})}{\u F (\dyn \times \dyn)}\cbvtocbpvcomp{(V_1,V_2)}\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} \times \cbvtocbpvty{A_2'})}{\u F (\dyn\times\dyn)}\defupcast{\u F (\cbvtocbpvty{A_1} \times \cbvtocbpvty{A_2})}{\u F (\dyn\times\dyn)}\ret(\cbvtocbpvval{V_1},\cbvtocbpvval{V_2})\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} \times \cbvtocbpvty{A_2'})}{\u F (\dyn\times\dyn)}(\ret\upcast{(\cbvtocbpvty{A_1} \times \cbvtocbpvty{A_2})}{(\dyn\times\dyn)}(\cbvtocbpvval{V_1},\cbvtocbpvval{V_2}))\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} \times \cbvtocbpvty{A_2'})}{\u F (\dyn\times\dyn)}\\
+      &\qquad(\ret (\pmpairWtoXYinZ {(\cbvtocbpvval{V_1},\cbvtocbpvval{V_2})} {x_1}{x_2}(\upcast{\cbvtocbpvty{A_1}}\dyn x_1, \upcast{\cbvtocbpvty{A_2}}\dyn x_2)))\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} \times \cbvtocbpvty{A_2'})}{\u F (\dyn\times\dyn)}(\ret (\upcast{\cbvtocbpvty{A_1}}\dyn {\cbvtocbpvval{V_1}}, \upcast{\cbvtocbpvty{A_2}}\dyn x_2))\\
+      &\equidyn
+      \pmpairWtoXYinZ {(\upcast{\cbvtocbpvty{A_1}}\dyn {\cbvtocbpvval{V_1}}, \upcast{\cbvtocbpvty{A_2}}\dyn {\cbvtocbpvval{V_2}})} {y_1}{y_2}\\
+      &\qquad
+      \bindXtoYinZ {\dncast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}\ret y_1} {x_1'}\\
+      &\qquad
+      \bindXtoYinZ {\dncast{\u F \cbvtocbpvty{A_2'}}{\u F \dyn}\ret y_2} {x_2'}
+      \ret (x_1',x_2')\\
+      &\equidyn
+      \bindXtoYinZ {\dncast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}\ret \upcast{\cbvtocbpvty{A_1}}\dyn {\cbvtocbpvval{V_1}}} {x_1'}\\
+      &\qquad
+      \bindXtoYinZ {\dncast{\u F \cbvtocbpvty{A_2'}}{\u F \dyn}\ret \upcast{\cbvtocbpvty{A_2}}\dyn {\cbvtocbpvval{V_2}}} {x_2'}
+      \ret (x_1',x_2')\\
+      &\equidyn
+      \bindXtoYinZ {\dncast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}\defupcast{\cbvtocbpvty{A_1}}\dyn {\ret\cbvtocbpvval{V_1}}} {x_1'}\\
+      &\qquad
+      \bindXtoYinZ {\dncast{\u F \cbvtocbpvty{A_2'}}{\u F \dyn}\defupcast{\cbvtocbpvty{A_2}}\dyn {\ret\cbvtocbpvval{V_2}}} {x_2'}
+      \ret (x_1',x_2')\\
+      &\equidyn
+      \bindXtoYinZ {\dncast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}\defupcast{\cbvtocbpvty{A_1}}\dyn {\cbvtocbpvcomp{V_1}}} {x_1'}\\
+      &\qquad
+      \bindXtoYinZ {\dncast{\u F \cbvtocbpvty{A_2'}}{\u F \dyn}\defupcast{\cbvtocbpvty{A_2}}\dyn {\cbvtocbpvcomp{V_2}}} {x_2'}
+      \ret (x_1',x_2')\\
+      &\equidyn
+      \bindXtoYinZ {\cbvtocbpvcomp{\obcast{A_1'}{A_1}V_1}} {x_1'}
+      \bindXtoYinZ {\cbvtocbpvcomp{\obcast{A_2'}{A_2}V_2}} {x_2'}
+      \ret (x_1',x_2')\\
+      &= \cbvtocbpvcomp{({\obcast{A_1'}{A_1}V_1}, {\obcast{A_2'}{A_2}V_2})}
+    \end{align*}
+  \item $\obcast{A_1' + A_2'}{A_1 + A_2}{(\inl V)} \step \obcast{A_1'}{A_1}V$
+    \begin{align*}
+      &\cbvtocbpvcomp{(\obcast{A_1' + A_2'}{A_1 + A_2}(\inl V))}\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} + \cbvtocbpvty{A_2'})}{\u F \dyn}\defupcast{\u F (\cbvtocbpvty{A_1} + \cbvtocbpvty{A_2})}{\u F \dyn}\cbvtocbpvcomp{(\inl V)}\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} + \cbvtocbpvty{A_2'})}{\u F (\dyn+\dyn)}\defupcast{\u F (\cbvtocbpvty{A_1} + \cbvtocbpvty{A_2})}{\u F (\dyn + \dyn)}\cbvtocbpvcomp{(\inl V)}\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} + \cbvtocbpvty{A_2'})}{\u F (\dyn+\dyn)}\defupcast{\u F (\cbvtocbpvty{A_1} + \cbvtocbpvty{A_2})}{\u F (\dyn+\dyn)}\ret(\inl \cbvtocbpvval V)\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} + \cbvtocbpvty{A_2'})}{\u F (\dyn+\dyn)}\ret\upcast{(\cbvtocbpvty{A_1} + \cbvtocbpvty{A_2})}{(\dyn+\dyn)}(\inl \cbvtocbpvval V)\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} + \cbvtocbpvty{A_2'})}{\u F (\dyn+\dyn)}\ret(\caseofXthenYelseZ {\inl \cbvtocbpvval V} {x_1. \inl \upcast{A_1}\dyn x_1}{x_2. \inr \upcast{A_2}\dyn x_2})\\
+      &\equidyn
+      \dncast{\u F (\cbvtocbpvty{A_1'} + \cbvtocbpvty{A_2'})}{\u F (\dyn+\dyn)}\ret(\inl \upcast{A_1}\dyn \cbvtocbpvval V)\\
+      &\equidyn
+      \caseofXthenYelseZ {(\inl \upcast{A_1}\dyn \cbvtocbpvval V)}
+      {x_1. \dncast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}\ret x_1}
+      {x_2. \dncast{\u F \cbvtocbpvty{A_2'}}{\u F \dyn}\ret x_2}\\
+      &\equidyn
+      {\dncast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}\ret \upcast{A_1}\dyn \cbvtocbpvval V}\\
+      &\equidyn {\dncast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}\defupcast{\u F A_1}{\u F \dyn}\ret \cbvtocbpvval V}\\
+      &\equidyn {\dncast{\u F \cbvtocbpvty{A_1'}}{\u F \dyn}\defupcast{\u F A_1}{\u F \dyn}\cbvtocbpvcomp V}\\
+      &\equidyn \cbvtocbpvcomp{(\obcast{A_1'}{A_1}V)}
+    \end{align*}
+  \item $\obcast{A_1' + A_2'}{A_1 + A_2}{(\inr V)} \step \obcast{A_2'}{A_2}V$: similar to $\inl$ case.
   \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}