diff --git a/paper/gtt.tex b/paper/gtt.tex
index 9365e9117ad7ea43cf38f844bbf66ba9c0e3c758..308e7bc9585ac65c4e0edd56dba4b462336b0419 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -3533,7 +3533,7 @@ Recall that for value types $A_1$ and $A_2$, the CBV function type is
 $U(A_1 \to \u F A_2)$.  As a corollary of
 Theorems~\ref{thm:functorial-casts} and
 \ref{thm:monadic-comonadic-casts}, we have
-\begin{corollary}[Cast for CBV Functions]
+\begin{corollary}[Cast Unique Implementation for CBV Functions]
   \[
   \begin{small}
   \begin{array}{l}
@@ -4024,12 +4024,12 @@ While contracts are typically implemented in a dynamically typed
 language, our target is typed, meaning we retain type information
 that might be used in later stages of compilation.
 
-Overall, the remaining sections of the paper establish
-the following theorems:
+Writing $\sem{M}$ for the contract translation, the remaining sections
+of the paper establish:
 \begin{theorem}[Equi-dynamism implies Observational Equivalence]
   If $\Gamma \vdash M_1 \equidyn M_2 : \u B$, then for any closing
-  context $C : (\Gamma \vdash \u B) \Rightarrow (\cdot \vdash \u F
-  (1+1))$, $C[M_1]$ and $C[M_2]$ have the same behavior: both diverge,
+  context GTT $C : (\Gamma \vdash \u B) \Rightarrow (\cdot \vdash \u F
+  (1+1))$, $\sem{C[M_1]}$ and $\sem{C[M_2]}$ have the same behavior: both diverge,
   both run to an error, or both run to $\tru$ or both run to $\fls$.
 \end{theorem}
 \begin{theorem}[Graduality]
@@ -4637,12 +4637,12 @@ This leads to the following definition:
   $(\dynv + \dynv) \cong ((1+1) \times \dynv)$ with the ep pair for
   $1+1$ using the action of product types on ep pairs (proven as part of
   Theorem \ref{thm:axiomatic-graduality}): $(\dynv + \dynv) \cong
-  ((1+1)\times \dynv) \triangleleft (\dynv \times \dynv) \triangleleft
+  ((1+1)\times \dynv) \,\triangleleft\, (\dynv \times \dynv) \,\triangleleft\,
   \dynv$ (where we write $A \triangleleft A'$ to mean there is an ep
   pair from $A$ to $A'$).  Similarly, for $\dync \with \dync$, we use
   action of the function type on ep pairs (also proven as part of
   Theorem \ref{thm:axiomatic-graduality}): $\dync \with \dync \cong
-  ((1+1) \to \dync) \triangleleft (\dynv \to \dync) \triangleleft \dync$
+  ((1+1) \to \dync) \,\triangleleft\, (\dynv \to \dync) \,\triangleleft\, \dync$
 \end{proof}
 
 \begin{shortonly}
@@ -4732,10 +4732,10 @@ form for $\dync$.
 The elimination form for $\dynv$ is a typed version of Scheme's
 \emph{match} macro.
 %
-Surprisingly, the introduction form for $\dync$ is very similar to a
+The introduction form for $\dync$ is very similar to a
 typed version of Scheme's \emph{case-lambda} construct.
 %
-Finally, we add \emph{type dynamisms} expressing the representations of
+Finally, we add type dynamism rules expressing the representations of
 $1$, $A + A$, and $A \times A$ in terms of booleans that were explicit
 in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
 \begin{shortonly}
@@ -5260,7 +5260,7 @@ 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 that it
+  (Section~\ref{sec:theorems-in-gtt}), and in the extened version 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.
@@ -6571,6 +6571,10 @@ strictness.)
 This translation clarifies the behavioral meaning of complex values and
 stacks, following \cite{munchmaccagnoni14nonassociative,
   fuhrmann1999direct}, and therefore of upcasts and downcasts.
+\begin{longonly}
+This is related to completeness of focusing: it moves inversion rules
+outside of focus phases.
+\end{longonly}
 
 \begin{longonly}
 The syntax of operational CBPV is as in
@@ -6912,8 +6916,8 @@ More formally, we translate a \cbpvstar\/ complex value $V : A$ to a
 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
+$\bullet : \u B$ to a \cbpv\  computation $\simp{S}$ with a 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
@@ -7018,7 +7022,7 @@ runing $M$ every time we need its value:
   \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\]
+  \[\Gamma \vdash \ret{( \thunk M)} \equidyn \bindXtoYinZ M x \ret{(\thunk (\ret x))} : \u FU\u F A\]
 \iflong
   \end{definition}
 \fi
@@ -7039,7 +7043,7 @@ $x$ exactly once, first, these two are the same.
 \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}
@@ -7066,9 +7070,9 @@ decomplexification.
 %%   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}.
+\noindent Composing this with the translation from GTT to \cbpvstar\/
+shows that \emph{GTT value upcasts are thunkable and computation
+  downcasts are linear}, which justifies a number of program transformations.
 \end{shortonly}
 
 \begin{longonly}