diff --git a/paper/gtt.tex b/paper/gtt.tex
index b5abb59f59243be80ebc096c89f21b385db7d328..2a61d07f74b73042869dd1aa375aa3e066203316 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -446,6 +446,7 @@ expressing the actual desired properties of the gradual language,
 which are \emph{program equivalences in the typed portion of the code} that are
 not valid in the dynamically typed portion. 
 
+\textbf{An Axiomatic Approach to Gradual Typing}
 In this paper, we systematically study questions of program equivalence
 for a class of gradually typed languages by working in an
 \emph{axiomatic theory} of gradual program equivalence, a language and
@@ -469,7 +470,6 @@ Gradual type theory can be used both to explore language design questions and
 to verify behavioral properties of specific programs, such as correctness of
 optimizations and refactorings.
 
-\textbf{FIXME: This needs a section header but I'm not sure what to call it.}
 To get off the ground, we take two properties of the gradual language
 for granted.
 %
@@ -632,14 +632,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$.
 
-%% FIXME: There should be some comment here that these aren't new
-%%   observations about transient/eager, and what our work adds\ldots Is
-%%   this right?
-  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$.
 The reader unfamiliar with proof theory may find the centrality of
 $\eta$ equalities in our development unusual.  
 %
@@ -651,10 +649,9 @@ restricted in a typed language to only hold for terms of function type $M
 This famously ``fails'' to hold in call-by-value languages in the presence
 of effects: if $M$ is a program that prints \texttt{"hello"} before returning a
 function, then $M$ will print \emph{now}, whereas $\lambda x. M x$ will only print
-when given an argument.  But this is also not an obstacle, because the $\eta$ law is
-valid in some call-by-value languages (e.g. SML) if we have a ``value
-restriction'' $V \equiv \lambda x. V x$ or otherwise restrict to non-effectful
-programs.
+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
+restriction'' $V \equiv \lambda x. V x$.
 %
 This illustrates that $\eta$/extensionality rules must be stated for each type
 connective, and be sensitive to the effects/evaluation order of the terms