diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index bb682ea7f5048b5b02f724c1b4b902b8ab9f20a7..a1d1a041e1b449161e9b179ab7c068bc4e4d5e6e 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -1943,9 +1943,10 @@ some relevant definitions and facts.
     \equidyn \bullet' : \u B'$.
   \end{enumerate}
 \end{definition}
-Note that a value isomorphism is a strong condition, and an isomorphism
-in call-by-value between types $A$ and $A'$ corresponds to a computation
-isomorphism $\u F A \cong \u F A'$, and dually~\cite{levy17popl}.
+Note that a value isomorphism is a strong condition, and an
+isomorphism in call-by-value between types $A$ and $A'$ corresponds to
+a computation isomorphism $\u F A \cong \u F A'$, and
+dually~\cite{levy17popl}.
 
 \smallskip
 
@@ -2009,8 +2010,7 @@ isomorphism $\u F A \cong \u F A'$, and dually~\cite{levy17popl}.
   are non-trivial computation types in this model.  
     \end{enumerate}
 \end{proof}
-  
-  \begin{lemma}[Terminal objects] ~ \label{lem:terminal}
+\begin{lemma}[Terminal objects] ~ \label{lem:terminal}
     \begin{enumerate}
     \item For any computation type $\u B$, there exists a unique stack
       $\bullet : \u B \vdash S : \top$.
@@ -2021,8 +2021,8 @@ isomorphism $\u F A \cong \u F A'$, and dually~\cite{levy17popl}.
     \item $U \top \cong_v 1$
     \item $\top$ is not a strict terminal object.  
     \end{enumerate}
-  \end{lemma}
-  \begin{proof} ~
+\end{lemma}
+\begin{proof} ~
     \begin{enumerate}
     \item Take $S = \{\}$.  The $\eta$ rule for $\top$, $\bullet : \top
       \vdash \bullet \equidyn \{\} : \top$, under the substitution of
@@ -2051,10 +2051,9 @@ isomorphism $\u F A \cong \u F A'$, and dually~\cite{levy17popl}.
       isomorphic to $\u F 0$ and $\top$.  But there are non-trivial
       computation types in the model.  
     \end{enumerate}
-  \end{proof}
+\end{proof}
 \end{longonly}
 
-\begin{longonly}
 \subsection{Derived Cast Rules}
 
 As noted above, monotonicity of type dynamism for $U$ and $\u F$ means
@@ -2186,7 +2185,21 @@ For the fourth, by downcast right, it suffices show
 $\dncast{\u B}{\u B''}{\bullet''}\ltdyn {\bullet''} : \u B \ltdyn \u B''$,
 which is true by downcast left.
 \end{longproof}
-\end{longonly}
+
+Next, while it is important to identify that upcasts between value
+types are pure values and downcasts between computation types are
+linear stacks, when dealing with a mix of upcasts and downcasts, it is
+often useful to use the following derived ``shifted'' upcasts and
+downcasts.
+
+\begin{definition}[Upcast stacks/Downcast values]
+  If $A \ltdyn A'$, then we define
+  \[ \defupcast{\u F A}{\u F A'}E = \bindXtoYinZ E x \ret\upcast{A}{A'}x.\]
+  If $\u B \ltdyn \u B'$ then we define
+  \[ \defdncast{U \u B}{U \u B'}V = \thunk (\dncast{\u B}{\u B'}(\force V))\]
+\end{definition}
+
+TODO
 
 \subsection{Type-Generic Properties of Casts}
 
@@ -3697,17 +3710,8 @@ rule is true for $\ltdyn'$, except $A \ltdyn \dynv$ and $\u B \ltdyn
 
 Let GTT$_G$ be the fragment of GTT where the only primitive casts are
 those between ground types and the dynamic types, i.e. the cast terms
-are restricted to the substitution closures of
-\[
-\begin{small}
-\begin{array}{llll}
-x : G \vdash \upcast{G}{\dynv}{x} : \dynv &
-\bullet : \u F \dynv \vdash \dncast{\u F G}{\u F \dynv}{\bullet} : \u F \dynv &
-\bullet : \dync \vdash \dncast{\u G}{\dync}{\bullet} : \dync &
-x : U \u G \vdash \upcast{U \u G}{U \dync}{x} : U \dync 
-\end{array}
-\end{small}
-\]
+are restricted to $\upcast G \dynv V, \dncast{\u F G}{\u F \dynv},
+\dncast{\u G}{\dync}E, \upcast{U \u G}{U \dync}E$.
 
 \begin{lemma}[Casts are Admissible] \label{lem:casts-admissible}
 In GTT$_G$ it is admissible that
@@ -4117,16 +4121,13 @@ of the operational behavior of a standard Call-by-value cast calculus.
   \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}}\\
+      \cbvtocbpvcomp{(\obcast \dyn G V)}
+      &= \dncast{F \dyn}{F \dyn}\defupcast{\u F {\cbvtocbpvty G}}{\u F \dyn}{\cbvtocbpvcomp V}\tag{defn.}\\
+      &\equidyn \defupcast{\u F {\cbvtocbpvty G}}{\u F \dyn}{\cbvtocbpvcomp V}\tag{Theorem~\ref{thm:decomposition}}\\
+      &= \bindXtoYinZ {\cbvtocbpvcomp V} x \ret {\upcast{\cbvtocbpvty G}{\dyn}x}\tag{defn.}\\
+      &\equidyn \bindXtoYinZ {\ret\cbvtocbpvval V} x \ret {\upcast{\cbvtocbpvty G}{\dyn}x}\tag{defn.}\\      
+      &\equidyn \ret {\upcast{\cbvtocbpvty G}{\dyn}{\cbvtocbpvval V}}\tag{$F\beta$}\\
+      &= \ret \cbvtocbpvval{(\obcast\dyn G V)} \tag{defn.}
     \end{align*}
   \item $\lambda x:A. M$: immediate by reflexivity.
   \item $()$: immediate by reflexivity.