diff --git a/paper/abstract.tex b/paper/abstract.tex
index 19f1fb96a2d80175a58a0a336f750fc40980d5ed..e876b0d08f27d74f2c580e693cc750a63c8e238d 100644
--- a/paper/abstract.tex
+++ b/paper/abstract.tex
@@ -5,7 +5,8 @@ type-based reasoning is preserved when moving from the fully static setting to a
 gradual one. But gradual type soundness does not imply that type-based
 refactorings and optimizations are still sound in the gradual language.  
 Unfortunately, establishing the correctness of program transformations is 
-technically difficult and often neglected in the metatheory of these languages. 
+technically difficult---requires proofs of program equivalence---and
+often neglected in the metatheory of these languages.  
 
 In this paper, we propose an \emph{axiomatic} account of program equivalence in a
 gradual cast calculus, which we formalize in a logic we call \emph{gradual type
diff --git a/paper/gtt.tex b/paper/gtt.tex
index b44876c6955c8229a68ea9a3f46faa4c75978bb8..865d6586b2af2df1fd7b94cf59833c2453952f45 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -378,6 +378,9 @@ different from full static typing: we already accept the possibility that
 another part of the program goes into an infinite loop, and all of our
 reasoning must be relative to that possibility.
 
+% AA: Let's make sure that following paragraph is understandable even if the
+% reader doesn't know difference between transient, eager, and lazy semantics. 
+
 However, the dichotomy between gradual and optional typing is not as
 firm as one might like.
 %