diff --git a/paper/gtt.tex b/paper/gtt.tex
index a64ce7918d39bb0a95f602696b8348f067af29fd..1fb49dfe8ab55c2be815a670774cf4e8404e7694 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -4031,6 +4031,7 @@ for observational equivalence and an operational semantics that
 satisfies the graduality theorem.
 
 \subsection{Call-by-push-value}
+\label{sec:cbpvstar}
 
 Next, we define the call-by-push-value language \cbpvstar\ that will be
 the target for our contract translations of GTT.
@@ -6524,8 +6525,9 @@ dynamisms that happen to be homogeneous) are sound and complete for
 inequalities in \cbpvstar.
 \begin{corollary}[Conservativity]
   If $\Gamma \mid \Delta \vdash E, E' : T$ are two terms of the same
-  type in GTT, then $\Gamma \mid \Delta \vdash E \ltdyn E' : T$ is
-  provable in GTT if and only if it is provable in \cbpvstar.
+  type in the intersection of GTT and \cbpvstar, then $\Gamma \mid
+  \Delta \vdash E \ltdyn E' : T$ is provable in GTT if and only if it is
+  provable in \cbpvstar.
 \end{corollary}
 \begin{proof}
   The reverse direction holds because \cbpvstar\ is a syntactic subset of
@@ -6540,31 +6542,36 @@ Next, to bridge the gap between the semantic notion of complex value
 and stack with the more rigid operational notion, we perform a
 complexity-elimination pass.
 %
-This translates terms with complex values in it to an equivalent term
-without complex values: i.e., all pattern matches take place in terms,
-rather than in values.
+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.
 %
 Though 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 where all computation introduction forms are in terms, rather
-than stacks.
+stacks without pattern-matching and computation introduction forms.
 %
-This also provides an operational meaning to complex values and
-stacks, which was established in (TODO: cite, duploids, fuhrmann).
-
-We present the syntax of operational CBPV in \ref{fig:operational-cbpv}.
-%
-Whereas before the values included the pattern matching forms, now
-they include only introduction forms, as usual for values in
-operational semantics.
-%
-Whereas before stacks were just terms with a single variable
-$\bullet$, here we explicitly distinguish them.
-%
-Dual to the treatment of values, stacks consist only of
-\emph{elimination} forms.
+This translation clarifies the behavioral meaning to complex values and
+stacks, following \cite{duploids, fuhrmann}, and therefore of upcasts
+and downcasts.
 
+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}
+  \[
+    V ::= x \mid \rollty{\mu X.A}V \mid \inl{V} \mid \inr{V} \mid () \mid (V_1,V_2)\mid \thunk{M}
+    \quad
+    S ::= \bullet \mid \bindXtoYinZ S x M \mid S\, V \mid \pi S \mid \pi' S \mid \unroll{S}
+    \]
+\end{small}
+\end{shortonly}
+\begin{longonly}
+  as in Figure~\ref{fig:operation-cbpv-syntax}.
+  
 \begin{figure}
 \begin{small}
   \begin{mathpar}
@@ -6573,20 +6580,27 @@ Dual to the treatment of values, stacks consist only of
     \u B  & ::= & \u Y\mid \nu \u Y. \u B \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
     \Gamma & ::= & \cdot \mid \Gamma, x : A \\
     \Delta  & ::= & \cdot \mid \bullet : \u B \\
-    V  & ::= & x \mid \rollty{\mu X.A}V \mid \inl{V} \mid \inr{V} \mid \\
-       & & () \mid (V_1,V_2)\mid \thunk{M}
+    V  & ::= & x \mid \rollty{\mu X.A}V \mid \inl{V} \mid \inr{V} \mid () \mid (V_1,V_2)\mid \thunk{M}
     \\
     M & ::= & \err_{\u B} \mid \letXbeYinZ V x M \mid \pmmuXtoYinZ V x M \mid \rollty{\nu \u Y.\u B} M \mid \unroll M \mid \abort{V} \mid \\
     & & \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2} \mid \pmpairWtoinZ V M \mid \pmpairWtoXYinZ V x y M
     \mid \force{V} \mid \\
     & & \ret{V} \mid \bindXtoYinZ{M}{x}{N} \mid \lambda x:A.M \mid M\,V \mid \emptypair \mid \pair{M_1}{M_2} \mid \pi M \mid \pi' M
     \\
-    S & ::= & \bullet \mid \bindXtoYinZ S x M \mid S\, V \mid \pi S \mid \pi' S
+    S & ::= & \bullet \mid \bindXtoYinZ S x M \mid S\, V \mid \pi S \mid \pi' S \mid \unrollty{\nu \u Y.\u B}{S}
   \end{array}
   \end{mathpar}
   \end{small}
-  \caption{Operational CBPV Syntax}
+\caption{Operational CBPV Syntax}
+\label{fig:operation-cbpv-syntax}
 \end{figure}
+\end{longonly}
+%
+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 (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).
 
 \begin{longfigure}
 \begin{small}
@@ -6858,95 +6872,50 @@ Dual to the treatment of values, stacks consist only of
   \caption{CBPV logical and error rules}
 \end{longfigure}
 
-With this in mind, how is it possible that we even \emph{can}
-``eliminate'' these forms: for closed values, we can ``evaluate away''
+\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.
+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.  
+\begin{longonly}
+For example, for a closed value, we could ``evaluate away''
 the complexity and get a closed simple value (if we don't use $U$), but
-for open terms, evaluation will get ``stuck'' when we pattern match on
-a variable.
-%
-The trick is that we do \emph{not} translate complex values to values
-and complex stacks to stacks.
-%
-Rather, we translate complex values $V : A$ to a term $\simp{V} : \u F
-A$ that in \cbpvstar\ is equivalent to $\ret V$, but doesn't use any
-complex values or stacks as subterms.
-%
-Similarly, we translate a complex stack $S$ with hole $\bullet : \u B$
-to a term $\simp{S}$ with a \emph{free variable} $z : U \u B$ such that
-in \cbpvstar, $\simp S \equidyn S[\force z]$.
-%
-While this is type changing values and stacks, ultimately terms $M$
-will be translated to terms $\simp{M}$ with the same type.
-
-The philosophy behind the translation is that ultimately we are
-concerned with the operational behavior of terms $\Gamma \vdash M : \u
-B$, and all uses of complex values and stacks are \emph{conveniences}
-for reasoning about terms $M$ and so can be cut-eliminated from any
-particular proof.
-%
-In order for this to be true, we need to preserve the $\beta,\eta$
-equations somehow in the complexity-elimination translation.
-%
-To do this inductively, we note that complex values and stacks are
-translated to terms that are each in some sense ``pure'' or ``total''.
-%
-Specifically, we show that complex values are translated to terms that
-satisfy a property called \emph{thunkability}, and dually, complex stacks are
-translated to terms that satisfy \emph{linearity} (terminology from TODO: cite
-fuhrmann, Guillaume MM). 
-
-A thunkable term is a term of type $M : \u F A$ that acts like $\ret
-V$.
-%
-Intuitively, this means $M$ should have no observable effects, and so
-can be freely duplicated or discarded like a value.
-%
-We can define this using the inequational theory of CBPV by saying
-that it doesn't matter if we run $M$ to a value and then duplicate the
-value or if we run $M$ every time we need its value.
-\begin{definition}[Thunkable Term]
-  A term $\Gamma \vdash M : \u FA$ is \emph{thunkable} if the following
-  is provable:
-  \[
-  \Gamma \vdash \ret \thunk M \equidyn \bindXtoYinZ M x \ret\thunk\ret x : \u FU\u F A
-  \]
-\end{definition}
-
-Dually, a term $M$ with a free variable $x : U \u B$ is linear in $x$
-if it acts like $S[\force x]$.
-%
-Complex stacks are syntactically linear terms if we consider $\bullet$
-as a variable, so a term is \emph{semantically} linear if it has the
-behavior that this implies.
-%
-Specifically a linear term is \emph{strict} in $x$ in that when the
-term is run (forced), it will force $x$.
-%
-This will allow us to prove the preservation of the $\eta$ principles
-for positive types and the strictness of complex stacks with respect
-to errors.
-%
-We can formalize this in the CBPV inequational theory with the
-following equation that intuitively says 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.
-\begin{definition}[Linear Term]
-  A term $\Gamma, x : U\u B \vdash M : \u C$ is \emph{linear in $x$}
-  if the following is provable:
-  \[
-  \Gamma, z : U\u FU\u B \vdash
-  \bindXtoYinZ {\force z} x M
-  \equidyn
-  M[\thunk{(\bindXtoYinZ {\force z} x \force x)}]
-  \]
-\end{definition}
+for open terms, evaluation will get ``stuck'' if we pattern match on
+a variable---so not every complex value can be translated to a value in
+\cbpv.  
+\end{longonly}
+More formally, we translate a \cbpvstar\/ complex value $V : A$ to a
+\cbpv\/ computation $\simp{V} : \u F A$ that in \cbpvstar\ is equivalent
+to $\ret V$.
+%
+Similarly, we translate a \cbpvstar\/ complex stack $S$ with hole
+$\bullet : \u B$ to a \cbpv\  computation $\simp{S}$ with a \emph{free
+  variable} $z : U \u B$ such that in \cbpvstar, $\simp S \equidyn
+S[\force z]$.
+%
+Computations $M : \u B$ are translated to computations $\simp{M}$ with
+the same type.
+%% This is sufficient because we view computations $\Gamma
+%% \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.
 
+\begin{longonly}
 The \emph{de-complexification} procedure is defined as follows.
 %
-We note that this translation is not the one presented in the CBPV
-monograph, but rather a more inefficient version that, in CPS terminology,
-introduces many administrative redices.
+We note that this translation is not the one presented in
+\cite{levybook}, but rather a more inefficient version that, in CPS
+terminology, introduces many administrative redices.
 %
 Since we are only proving results up to observational equivalence
 anyway, the difference doesn't change any of our theorems, and makes
@@ -6982,29 +6951,77 @@ some of the proofs simpler.
   \end{mathpar}
   \end{small}
 \end{definition}
-
+\end{longonly}
+The translation is type-preserving
 \begin{lemma}[De-complexification De-complexifies]
-  For any $\Gamma \pipe \Delta \vdash E : T$, $\simp E$ is a term of
-  operational CBPV satisfying
-  \[ \Gamma, \simp\Delta \vdash \simp E : \simp T \]
-  where
-  \begin{mathpar}
-    \simp{\cdot} = \cdot \and \simpp{\bullet:\u B} = z:U\u B\and
-    \simp{\u B} = \u B \and \simp A = \u F A
-  \end{mathpar}  
+  For any \cbpvstar\/ term $\Gamma \pipe \Delta \vdash E : T$, $\simp E$
+  is a term of \cbpv\/ satisfying $\Gamma, \simp\Delta \vdash \simp E :
+  \simp T$ where
+  $\simp{\cdot} = \cdot$ $\simpp{\bullet:\u B} = z:U\u B$,
+  $\simp{\u B} = \u B$, $\simp A = \u F A$.
 \end{lemma}
-
+\noindent and is the identity from \cbpvstar's point of view
 \begin{lemma}[De-complexification is Identity in \cbpvstar]
-  Considering CBPV as a subset of \cbpvstar\, we can show
+  Considering CBPV as a subset of \cbpvstar\, we have
   \begin{enumerate}
   \item If $\Gamma \pipe \cdot \vdash M : \u B$  then $M \equidyn \simp M$.
   \item If $\Gamma \pipe \Delta \vdash S : \u B$ then $S[\force z] \equidyn \simp S$.
   \item If $\Gamma \vdash V : A$ then $\ret V \equidyn \simp V$.
   \end{enumerate}
-  Furthermore, if $M, V, S$ are in operational CBPV, the proof holds
-  in operational CBPV.
+  Furthermore, if $M, V, S$ are in \cbpv, the proof holds in \cbpv.
 \end{lemma}
 
+Finally, we need to show that the translation preserves inequalities
+($\simp{E} \ltdyn \simp{E'}$ if $E \ltdyn E'$), but because complex
+values and stacks satisfy more equations than arbitrary computations in
+the types of their translations do, we need to isolate the special
+``purity'' property that their translations have.
+%
+We show that complex values are translated to computations that satisfy
+\emph{thunkability}~\cite{gmm}, which
+%% DRL: I don't like this gloss for explaining the semantic property
+%% because it depends on the language V is in.  
+%% , where a thunkable computation is a
+%% computation of type $M : \u F A$ that acts like $\ret V$ does in
+%% \cbpvstar.
+%
+intuitively means $M$ should have no observable effects, and so
+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 the
+  following is provable:
+  \[
+  \Gamma \vdash \ret \thunk M \equidyn \bindXtoYinZ M x \ret\thunk\ret x : \u FU\u F A
+  \]
+\end{definition}
+Dually, we show that complex stacks are translated to computations that
+satisfy (semantic) \emph{linearity}, 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
+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 the following is provable:
+  \[
+  \Gamma, z : U\u FU\u B \vdash
+  \bindXtoYinZ {\force z} x M
+  \equidyn
+  M[\thunk{(\bindXtoYinZ {\force z} x \force x)}]
+  \]
+\end{definition}
+Thunkability/linearity of the translations of complex values/stacks are
+useed to prove the preservation of the $\eta$ principles for positive
+types and the strictness of complex stacks with respect to errors under
+decomplexification.
+
 \begin{longonly}
 We need a few lemmas about thunkables and linears to prove that
 complex values become thunkable and complex stacks become linear.
@@ -7355,12 +7372,8 @@ composition.
 
 
 \begin{theorem}[De-complexification preserves Dynamism]
-  \[
-    \begin{small}
-\inferrule{\Gamma \pipe \Delta \vdash E \ltdyn E' : T}{\Gamma, \simp \Delta
-  \vdash \simp E \ltdyn \simp{E'} : \simp T}
-  \end{small}
-  \]
+  If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then ${\Gamma, \simp
+    \Delta \vdash \simp E \ltdyn \simp{E'} : \simp T}$
 \end{theorem}
 \begin{longproof}
   $\beta$ axioms need to reduce administrative redices ugh