diff --git a/paper/abstract.tex b/paper/abstract.tex
index 2a88a2724f85c40a094d42b31330bde53e07d6a9..9799d9152d71d4cd257b1fbaf9fcd551b0dcba7a 100644
--- a/paper/abstract.tex
+++ b/paper/abstract.tex
@@ -22,8 +22,7 @@ connective must be equivalent to the so-called ``lazy'' cast semantics.
 Contrapositively, this shows that ``eager'' cast semantics violates the
 extensionality of function types.  As another example, we show that
 gradual upcasts are pure functions and, dually, gradual downcasts are
-strict functions, an equational analogue of Wadler-Findler's blame
-soundness theorem.  We show the consistency and applicability of our
+strict functions.  We show the consistency and applicability of our
 axiomatic theory by proving that a contract-based implementation using
 the lazy cast semantics gives a logical relations model of our type
 theory, where equivalence in GTT implies contextual equivalence of the
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 5af4f971d2c6a5c70b60e30e3b2b992003a9ed5c..f0280c8a4550943c5ad5f4d480c762750a1926be 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -466,8 +466,7 @@ $\lambda x. M x$ will only print when given an argument. But this can be
 accomodated with one further modification: the $\eta$ law is valid in
 simple call-by-value languages\footnote{This does not hold in languages
   with some intensional feature of functions such as reference
-  equality. We discuss the applicability of this theorem more generally
-  in section \ref{sec:related}} (e.g. SML) if we have a ``value
+  equality. We discuss the applicability of our main results more generally in section \ref{sec:related}} (e.g. SML) if we have a ``value
 restriction'' $V \equiv \lambda x. V x$.
 %
 This illustrates that $\eta$/extensionality rules must be stated for
@@ -689,11 +688,12 @@ valid inhabitant of that type.
 In summary the ``eager'' cast semantics is in fact overly eager: in
 its effort to find bugs faster than ``lazy'' semantics it disables the
 very type-based reasoning that gradual typing should provide.
-% FIXME
-While these criticisms of transient and eager cast semantics are
-well-known (cite?), a novel consequence of our development is that
-\emph{only} the lazy cast semantics satisifies both graduality and
-$\eta$.
+
+While criticisms of transient semantics on the basis of type soundness
+have been made before \citep{greenmanfelleisen:2018}, our development
+shows that the $\eta$ principles of types are enough to uniquely
+determine a cast semantics, and helps clarify the trade-off between
+eager and lazy semantics of function casts.
 
 \textbf{Technical Overview of GTT.}  The gradual type theory developed
 in this paper unifies our previous work~\citep{newahmed18} on
@@ -9608,7 +9608,7 @@ principles of local state.
 \fi
 We do not give a treatment of runtime blame reporting, but we argue that
 the observation that upcasts are thunkable and downcasts are linear is
-directly related to blame soundness~\cite{wadler-findler09} in that if
+directly related to blame soundness~\cite{tobin-hochstadt06,wadler-findler09} in that if
 an upcast were \emph{not} thunkable, it should raise positive blame and
 if a downcast were \emph{not} linear, it should raise negative blame.
 %