diff --git a/paper/gtt.tex b/paper/gtt.tex
index 2dd4f8a685509e5aa812e9888b5c04360f98af14..c94b41a8bb3249c6fbbec325a7825c4d44a883a5 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -458,8 +458,7 @@ the other does not) results.
 The logic axiomatizes the equational properties gradual
 programs should satisfy, and offers a high-level syntax for proving
 theorems about many languages at once:
-if a particular operational
-semantics models gradual type theory, then it satisfies all
+if a language models gradual type theory, then it satisfies all
 provable equivalences/approximations.
 %
 Due to its type-theoretic design, different axioms of program
@@ -9355,7 +9354,7 @@ Corollary~\ref{cor:contextual-decomposition} that this coincides with
 contextual equivalence.
 \end{longproof}
 
-\section{Related and Future Work}
+\section{Discussion and Related Work}
 \label{sec:related}
 
 In this paper, we have given a logic for reasoning about gradual
@@ -9393,7 +9392,7 @@ sections \ref{sec:contract}, \ref{sec:complex}, \ref{sec:operational}.
 We conjecture that simple call-by-value and call-by-name gradual
 languages are also models of GTT, by extending the translation of
 call-by-push-value into call-by-value and call-by-name in the appendix
-to Levy's monograph \cite{levy03cbpvbook}.
+of Levy's monograph \cite{levy03cbpvbook}.
 %
 In order for the theorem to apply, the language must validate an
 appropriate version of the $\eta$ principles for the types.
@@ -9402,10 +9401,10 @@ So for example, a call-by-value language that has reference equality
 of functions does \emph{not} validate even the value-restricted $\eta$
 law for functions, and so the case for functions does not apply.
 %
-It is a well-known issue that the lazy semantics of function casts is
-not compatible with the refinement property that graduality models in
-the presence of pointer equality, and our uniqueness theorem provides
-a different perspective on this phenomenon
+It is a well-known issue that in the presence of pointer equality of
+functions, the lazy semantics of function casts is not compatible with
+the graduality property, and our uniqueness theorem provides a
+different perspective on this phenomenon
 \cite{findlerflattfelleisen04,chaperonesimpersonators, refined}.
 %
 However, we note that the cases of the uniqueness theorem for each
@@ -9414,9 +9413,9 @@ specification of casts and the $\beta,\eta$ principles for the
 particular connective, and not on the presence of any other types,
 even the dynamic types.
 %
-So while a call-by-value language that has reference equality of
-functions might still have the $\eta$ principle for strict pairs, so
-that case of the theorem still applies.
+So even if a call-by-value language may have reference equality
+functions, if it has the $\eta$ principle for strict pairs, then the
+pair cast must be that of theorem \ref{functorial-casts}.
 
 Next, we consider the applicability to non-eager languages.
 %
@@ -9522,7 +9521,8 @@ related to our model construction in section
 \ref{sec:contract}.
 %
 More specifically, many of the lemmas proven in the extended version
-of the paper have direct analogues in Henglein's work.
+of this paper \citep{newlicataahmed19:extended} have direct analogues
+in Henglein's work.
 %
 We have not included these lemmas in the paper because they are quite
 similar to lemmas proven in \citet{newahmed18}; see there for a