diff --git a/paper/gtt.tex b/paper/gtt.tex
index 50ff6027adb630cf167d7235cceef03c5b90fc82..fb54a27749eabd2e7b539bc284cc58bb4b01a357 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -637,7 +637,7 @@ theory, but for only function and pair types in call-by-name (whereas
 all existing gradual languages are call-by-value), and gives
 domain-theoretic but not operational models of the axioms.
 
-In this paper, we develop an axiomatic gradual type theory for a unified
+In this paper, we develop an axiomatic gradual type theory GTT for a unified
 language that includes \emph{both} call-by-value/eager types and
 call-by-name/lazy types (Sections~\ref{sec:gtt}, \ref{sec:theorems-in-gtt}), and
 show that it is sound for contextual equivalence via a logical relations model
@@ -650,8 +650,8 @@ embeds both call-by-value and call-by-name evaluation with both eager and lazy
 datatypes,\footnote{The distinction between ``lazy'' vs ``eager'' casts above is
   different than lazy vs. eager datatypes.}  and underlies much recent work on
 reasoning about effectful programs~\cite{bauerpretnar13eff,lindley+17frank}.
-This gradual type theory can prove results in and about existing call-by-value gradually typed
-languages, and also suggests a design for call-by-name and even full
+GTT can prove results in and about existing call-by-value gradually typed
+languages, and also suggests a design for call-by-name and full
 call-by-push-value gradually typed languages.
 
 In the proior work on call-by-name gradual type
@@ -697,7 +697,9 @@ as a product of all possible behaviors.  At the language design level,
 gradual type theory can be used to prove that, for a variety of
 eager/value and lazy/computation types, the ``lazy contract'' semantics
 of casts is the unique implementation satisfying $\beta,\eta$ and
-graduality (Section~\ref{sec:theorems-in-gtt}).  
+graduality (Section~\ref{sec:theorems-in-gtt}). These behavioral
+equivalences can then be used in reasoning about optimizations,
+refactorings, and correctness of specific programs.  
 
 %% Morever, working in a setting with mixed eager/value and
 %% lazy/computation types often leads to more insight into each than