diff --git a/paper/gtt.tex b/paper/gtt.tex
index e5c6fe31f0315992949ef84ade07691e21e4e2b1..109d25af5d4d8e5e9098c87e2b4211b6e61ce388 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -5163,8 +5163,8 @@ a unique complex stack $x : \u B \vdash \supcast{\u B}{\u B'}{x} : \u B'$
 \subsubsection{Interpretation of Terms}~
 \end{longonly}
 \ Next, we extend the translation of casts to a translation of all terms
-by congruence, since all terms constructors in GTT besides casts are
-constructors in \cbpvstar.  This satisfies:
+by congruence, since all terms in GTT besides casts are
+in \cbpvstar.  This satisfies:
 \begin{lemma}[Contract Translation Type Preservation]
   If $\Gamma\pipe\Delta \vdash E : T$ in GTT, then $\sem{\Gamma}
   \pipe\sem\Delta\vdash \sem E : \sem T$ in \cbpvstar.
@@ -5229,10 +5229,12 @@ translate a heterogeneous term dynamism to a homogeneous inequality
   \end{longonly}
 \end{theorem}
 
-Relative to previous work on graduality (\cite{newahmed2018}),
+\begin{longonly}
+  Relative to previous work on graduality (\cite{newahmed18}),
 the distinction between complex value upcasts and complex stack
 downcasts guides the formulation of the theorem; e.g. using upcasts in
 the left-hand theorem would require more thunks/forces.  
+\end{longonly}
 
 \begin{shortonly}
   The full proof can be found in the extended version, and uses a
@@ -5254,10 +5256,10 @@ the left-hand theorem would require more thunks/forces.
   $\supcast{A}{A'}$ is equivalent to the identity and
   $\supcast{A'}{A''}\supcast{A}{A'}$ is $\supcast{A}{A''}$, and
   similarly for downcasts.  All of these properties are theorems in GTT
-  (Section~\ref{sec:theorems-in-gtt}), and the extened version in the
-  supplementary materials shows that it takes quite a bit of work to prove
-  them true in the model, which illustrates that the axiomatic theory of
-  GTT encodes a lot of information with relatively few rules.  
+  (Section~\ref{sec:theorems-in-gtt}), and the extened version that it
+  takes quite a bit of work to prove them true under translation, which
+  illustrates that the axiomatic theory of GTT encodes a lot of
+  information with relatively few rules.
 \end{shortonly}
 
 \begin{longonly}
@@ -6529,8 +6531,7 @@ introduction/elimination forms, and are all simple calculations.
 \end{longonly}
 
 As a corollary, we have the following conservativity result, which says
-that the homogeneous inequalities in GTT (i.e. those heterogeneous term
-dynamisms that happen to be homogeneous) are sound and complete for
+that the homogeneous term dynamaisms in GTT are sound and complete for
 inequalities in \cbpvstar.
 \begin{corollary}[Conservativity] \label{thm:gtt-cbpvstar-conservativity}
   If $\Gamma \mid \Delta \vdash E, E' : T$ are two terms of the same
@@ -6553,35 +6554,37 @@ complexity-elimination pass.
 %
 This translates a computation with complex values in it to an equivalent
 computation without complex values: i.e., all pattern matches take place
-in computations, rather than in values.
+in computations, rather than in values, and translates a term dynamism
+derivation that uses complex stacks to one that uses only ``simple''
+stacks without pattern-matching and computation introduction forms.
 %
-Though stacks do not appear anywhere in the grammar of terms, they are
+\begin{longonly}
+  Stacks do not appear anywhere in the grammar of terms, they are
 used in the equational theory (computation $\eta$ rules and error
-strictness), so we additionally translate complex stacks to ``simple''
-stacks without pattern-matching and computation introduction forms.
+strictness.)
+\end{longonly}
 %
-This translation clarifies the behavioral meaning to complex values and
-stacks, following \cite{duploids, fuhrmann}, and therefore of upcasts
-and downcasts.
+This translation clarifies the behavioral meaning of complex values and
+stacks, following \cite{munchmaccagnoni14nonassociative,
+  fuhrmann1999direct}, and therefore of upcasts and downcasts.
 
+\begin{longonly}
 The syntax of operational CBPV is as in
 Figure~\ref{fig:gtt-syntax-and-terms} (unshaded), but with recursive
 types added as in Section~\ref{sec:cbpvstar}, and with values and stacks
 restricted
-\begin{shortonly}
-to
-\begin{small}
-  \[
-  \begin{array}{l}
-    V ::= x \mid \rollty{\mu X.A}V \mid \inl{V} \mid \inr{V} \mid () \mid (V_1,V_2)\mid \thunk{M}\\
-    S ::= \bullet \mid \bindXtoYinZ S x M \mid S\, V \mid \pi S \mid \pi' S \mid \unroll{S}
-  \end{array}
-  \]
-\end{small}
-\end{shortonly}
-
-\iflong
-  as in Figure~\ref{fig:operation-cbpv-syntax}.
+%% \begin{shortonly}
+%% to
+%% \begin{small}
+%%   \[
+%%   \begin{array}{l}
+%%     V ::= x \mid \rollty{\mu X.A}V \mid \inl{V} \mid \inr{V} \mid () \mid (V_1,V_2)\mid \thunk{M}\\
+%%     S ::= \bullet \mid \bindXtoYinZ S x M \mid S\, V \mid \pi S \mid \pi' S \mid \unroll{S}
+%%   \end{array}
+%%   \]
+%% \end{small}
+%% \end{shortonly}
+as in Figure~\ref{fig:operation-cbpv-syntax}.
   
 \begin{figure}
 \begin{small}
@@ -6605,19 +6608,15 @@ to
 \caption{Operational CBPV Syntax}
 \label{fig:operation-cbpv-syntax}
 \end{figure}
-\fi
 %
 In \cbpv, values include only introduction forms, as usual for values in
 operational semantics, and \cbpv\/ stacks consist only of elimination
 forms for computation types
-\begin{longonly}
 (the syntax of \cbpv\/ enforces an A-normal
 form, where only values can be pattern-matched on, so $\kw{case}$ and
-$\kw{split}$ are not evaluation contexts in the operational semantics)
-\end{longonly}
-.
+$\kw{split}$ are not evaluation contexts in the operational semantics).
 
-\begin{longfigure}
+\begin{figure}
 \begin{small}
   \begin{mathpar}
     \inferrule
@@ -6730,9 +6729,9 @@ $\kw{split}$ are not evaluation contexts in the operational semantics)
   \end{mathpar}
   \end{small}
   \caption{CBPV Inequational Theory (Congruence Rules)}
-\end{longfigure}
+\end{figure}
 
-\begin{longfigure}
+\begin{figure}
 \begin{small}
   \begin{mathpar}
     \inferrule
@@ -6821,9 +6820,9 @@ $\kw{split}$ are not evaluation contexts in the operational semantics)
   \end{mathpar}
   \end{small}
   \caption{CBPV $\beta, \eta$ rules}
-\end{longfigure}
+\end{figure}
 
-\begin{longfigure}
+\begin{figure}
 \begin{small}
   \begin{mathpar}
     \inferrule
@@ -6885,11 +6884,15 @@ $\kw{split}$ are not evaluation contexts in the operational semantics)
   \end{mathpar}
   \end{small}
   \caption{CBPV logical and error rules}
-\end{longfigure}
+\end{figure}
+
+\end{longonly}
 
-\cite{levybook} translates \cbpvstar\/ to \cbpv, but not does not prove
-the inequality preservation that we require here, so we give an
-alternative translation for which this property is easy to verify.
+Levy~\cite{levy03cbpvbook} translates \cbpvstar\/ to \cbpv, but not does not prove
+the inequality preservation that we require here, so we give
+an
+alternative translation for which this property is easy to
+verify \ifshort (see the extended version for full details)\fi.
 We translate both complex values and complex
 stacks to fully generaly computations, so that computation
 pattern-matching can replace the pattern-matching in complex values/stacks.  
@@ -6915,14 +6918,15 @@ the same type.
 %% \vdash M : \u B$ as the entry point of a program, so all uses of complex
 %% values and stacks are \emph{conveniences} for reasoning about
 %% computations, and so can be cut-eliminated from any particular proof.
-The full translation is in the extended version, and is defined by a
-simple structural induction that sequences the evaluation of the
-translation of each complex value, e.g.
-$\simpp{\caseofXthenYelseZ V {x_1. E_1}{x_2. E_2}} = 
-  \bindXtoYinZ {\simp V} x \caseofXthenYelseZ x {x_1. \simp {E_1}}{x_2. \simp {E_2}}$.
-We could replace this translation with one as in \cite{levybook} that
-introduces fewer administrative redices, but this translation is simpler
-and suffices for reasoning up to observational equivalence.
+%% 
+%% The full translation is in the extended version, and is defined by a
+%% simple structural induction that sequences the evaluation of the
+%% translation of each complex value, e.g.
+%% $\simpp{\caseofXthenYelseZ V {x_1. E_1}{x_2. E_2}} = 
+%%   \bindXtoYinZ {\simp V} x \caseofXthenYelseZ x {x_1. \simp {E_1}}{x_2. \simp {E_2}}$.
+%% We could replace this translation with one as in \cite{levybook} that
+%% introduces fewer administrative redices, but this translation is simpler
+%% and suffices for reasoning up to observational equivalence.
 
 \begin{longonly}
 The \emph{de-complexification} procedure is defined as follows.
@@ -6965,7 +6969,7 @@ some of the proofs simpler.
   \end{mathpar}
   \end{small}
 \end{definition}
-\end{longonly}
+
 The translation is type-preserving and the identity from \cbpvstar's point of view
 \begin{lemma}[De-complexification De-complexifies]
   For any \cbpvstar\/ term $\Gamma \pipe \Delta \vdash E : T$, $\simp E$
@@ -6984,6 +6988,7 @@ The translation is type-preserving and the identity from \cbpvstar's point of vi
   \end{enumerate}
   Furthermore, if $M, V, S$ are in \cbpv, the proof holds in \cbpv.
 \end{lemma}
+\end{longonly}
 
 Finally, we need to show that the translation preserves inequalities
 ($\simp{E} \ltdyn \simp{E'}$ if $E \ltdyn E'$), but because complex
@@ -7004,48 +7009,60 @@ can be freely duplicated or discarded like a value.
 %
 In the inequational theory of \cbpv\/, this is defined by saying that
 running $M$ to a value and then duplicating its value is the same as
-runing $M$ every time we need its value.
-\begin{definition}[Thunkable Computation]
-  A computation $\Gamma \vdash M : \u FA$ is \emph{thunkable} if \\
-  $\Gamma \vdash \ret \thunk M \equidyn \bindXtoYinZ M x \ret\thunk\ret x : \u FU\u F A$
-\end{definition}
+runing $M$ every time we need its value:
+\iflong{
+  \begin{definition}[Thunkable Computation]
+    A computation $\Gamma \vdash M : \u FA$ is \emph{thunkable} if \\
+\fi
+  \[\Gamma \vdash \ret \thunk M \equidyn \bindXtoYinZ M x \ret(\thunk (\ret x)) : \u FU\u F A\]
+\iflong
+  \end{definition}
+\fi
 Dually, we show that complex stacks are translated to computations that
 satisfy (semantic) \emph{linearity}~\cite{munchmaccagnoni14nonassociative}, where intuitively a computation $M$
 with a free variable $x : U \u B$ is linear in $x$ if $M$ behaves as if
 when it is forced, the first thing it does is forces $x$, and that is the only time
 it uses $x$.  This is described in the CBPV inequational theory as
-follows: if we have a thunk $z : U\u F U \u B$, then either we can force
+follows:
+\iflong
+if we have a thunk $z : U\u F U \u B$, then either we can force
 it now and pass the result to $M$ as $x$, or we can just run $M$ with a
 thunk that will force $z$ each time $M$ is forced---but if $M$ forces
 $x$ exactly once, first, these two are the same.
 \begin{definition}[Linear Term]
   A term $\Gamma, x : U\u B \vdash M : \u C$ is \emph{linear in $x$}
   if\\
-  $\Gamma, z : U\u FU\u B \vdash
+\fi
+ \[ \Gamma, z : U\u FU\u B \vdash
   \bindXtoYinZ {\force z} x M
-  \equidyn
-  M[\thunk{(\bindXtoYinZ {\force z} x \force x)}]$
+  \equidyn M[\thunk{(\bindXtoYinZ {\force z} x \force x)}]
+  \]
+\iflong
 \end{definition}
-Thunkability/linearity of the translations of complex values/stacks are
+\fi
+\begin{longonly}
+  Thunkability/linearity of the translations of complex values/stacks are
 used to prove the preservation of the $\eta$ principles for positive
 types and the strictness of complex stacks with respect to errors under
 decomplexification.
+\end{longonly}
+
 \begin{shortonly}
-  We have
-  \begin{theorem}[Soundness and Conservativity of De-Complexification] ~~
-    \begin{enumerate}
-    \item 
-    If $\Gamma \vdash V : A$ is a (possibly) complex value, then $\Gamma
-  \vdash \simp V : \u F A$ is thunkable.
-\item   If $\Gamma\pipe \bullet : \u B \vdash S : \u C$ is a (possibly)
-  complex stack, then $\Gamma, z : U\u B \vdash \simpp{S} : \u C$ is linear in $z$.
-\item   If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then ${\Gamma, \simp
-  \Delta \vdash \simp E \ltdyn \simp{E'} : \simp T}$.
-\item   If $M, M'$ are terms in CBPV and $M \ltdyn M'$ in \cbpvstar\ 
-  then $M \ltdyn M'$ in CBPV.
-    \end{enumerate}
-  \end{theorem}
-Composing this with the previous translation from GTT to \cbpvstar\/
+%%   \smallskip
+%%   \begin{theorem}[Soundness and Conservativity of De-Complexification] ~~
+%%     \begin{enumerate}
+%%     \item 
+%%     If $\Gamma \vdash V : A$ is a (possibly) complex value, then $\Gamma
+%%   \vdash \simp V : \u F A$ is thunkable.
+%% \item   If $\Gamma\pipe \bullet : \u B \vdash S : \u C$ is a (possibly)
+%%   complex stack, then $\Gamma, z : U\u B \vdash \simpp{S} : \u C$ is linear in $z$.
+%% \item   If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then ${\Gamma, \simp
+%%   \Delta \vdash \simp E \ltdyn \simp{E'} : \simp T}$.
+%% \item   If $M, M'$ are terms in CBPV and $M \ltdyn M'$ in \cbpvstar\ 
+%%   then $M \ltdyn M'$ in CBPV.
+%%     \end{enumerate}
+%%   \end{theorem}
+Composing this translation with the previous translation from GTT to \cbpvstar\/
 shows that \emph{GTT value type upcasts are thunkable and computation
   type downcasts are linear}.
 \end{shortonly}