diff --git a/paper/gtt.tex b/paper/gtt.tex
index 77409cb0c9d44a48e7feb8bfe50f7561ae6d1f27..6a15c56810198f69b70a351257ffaed7f89ed69d 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -9316,11 +9316,11 @@ contextual equivalence.
 \section{Related and Future Work}
 \label{sec:related}
 
-In this paper, we have given an axiomatic logic for reasoning about
-gradual programs in a mixed call-by-value/call-by-name language, shown
-that the axioms imply almost all of a contract translation implementing
-runtime casts, and shown that the axiomatics is sound for contextual
-equivalence/approximation in an operational model.
+In this paper, we have given a logic for reasoning about gradual
+programs in a mixed call-by-value/call-by-name language, shown that
+the axioms uniquely determine almost all of the contract translation
+implementing runtime casts, and shown that the axiomatics is sound for
+contextual equivalence/approximation in an operational model.
 \iflong
 
 \fi
@@ -9383,23 +9383,17 @@ Finally note that once we have introduced the extra thunks to model
 difference between call-by-name and call-by-need is only relevant for
 performance reasons.
 %
-Therefore the resulting semantics we produce should also be relevant
-for call-by-need evaluation.
-
-
-Some recent work \cite{greenmanfelleisen:2018} gives a spectrum of
-differing syntactic type soundness theorems for different semantics of
-gradual typing.
-%
-Our work here is complementary, showing that certain program
-equivalences can only be achieved by certain cast semantics.
+Therefore the resulting cast semantics we produce should also be
+valid for call-by-need evaluation.
 
 \citet{Degen2012TheIO} give an analysis of different cast semantics
-for contracts in lazy contracts.
+for contracts in lazy languages, specifically based on Haskell, so
+call-by-need with \texttt{seq}.
 %
 They propose two properties ``meaning preservation'' and
 ``completeness'' that they show are incompatible and identify which
-lazy contract semantics satisfy which of the properties.
+contract semantics for a lazy language satisfy which of the
+properties.
 %
 The meaning preservation property is closely related to graduality: it
 says that evaluating a term with a contract either produces blame or
@@ -9417,20 +9411,28 @@ The two properties are incompatible because for instance a pair of a
 diverging term and a value can't be deeply checked without causing the
 entire program to diverge.
 %
-Their observation is compatible with our main theorem in the following
-sense.
+Assuming we can extend the translation of call-by-name with
+\texttt{seq} to call-by-push-value, then their incompatibility theorem
+should be a consequence of our main theorem in the following sense.
 %
-We showed that the combination of $\eta$ principles and graduality
-implies the type-directed lazy contract semantics.
+Our main theorem shows that any semantics departing from the lazy
+semantics must violate $\eta$ or graduality.
 %
-Their completeness property is not satisfied by lazy contract checking
-(as they show), and so our theorems show that either the $\eta$
-principle or graduality is violated.
+Their completeness property is inherently eager, and so is different
+from the semantics GTT would provide, so either $\eta$ or graduality
+fails.
 %
-Since they are working with contracts defined within a call-by-name
-language, the $\eta$ principles do hold and so it must be graduality
-that fails, which corresponds to their failure of meaning
-preservation.
+However, since they are defining contracts within the language, they
+satisfy the restricted $\eta$ principle provided by the language, and
+so it must be graduality, and therefore meaning preservation that
+fails.
+
+Some recent work \cite{greenmanfelleisen:2018} gives a spectrum of
+differing syntactic type soundness theorems for different semantics of
+gradual typing.
+%
+Our work here is complementary, showing that certain program
+equivalences can only be achieved by certain cast semantics.
 
 Henglein's work on dynamic typing also uses an axiomatic semantics of
 casts, but axiomatizes behavior of casts at each type directly whereas
@@ -9439,7 +9441,7 @@ for each type \cite{henglein94:dynamic-typing}.
 %
 Because of this, the theorems proven in that paper are more closely
 related to our model construction in section
-\secref{sec:contract-models}.
+\ref{sec:contract-models}.
 %
 More specifically, many of the lemmas proven in the extended version
 of the paper have direct analogues in Henglein's work.