diff --git a/paper/gtt.tex b/paper/gtt.tex
index c94b41a8bb3249c6fbbec325a7825c4d44a883a5..be8c93c95ac5235149884e1aadc10a067cffbc37 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -9520,13 +9520,13 @@ Because of this, the theorems proven in that paper are more closely
 related to our model construction in section
 \ref{sec:contract}.
 %
-More specifically, many of the lemmas proven in the extended version
-of this paper \citep{newlicataahmed19:extended} have direct analogues
-in Henglein's work.
+More specifically, many of the properties of casts needed to prove
+theorem \ref{thm:axiomatic-graduality} have direct analogues
+in Henglein's work, such as the coherence theorems.
 %
 We have not included these lemmas in the paper because they are quite
-similar to lemmas proven in \citet{newahmed18}; see there for a
-more detailed comparison.
+similar to lemmas proven in \citet{newahmed18}; see there for a more
+detailed comparison, and the extended version of this paper for full proof details \citep{newlicataahmed19:extended}.
 %
 Finally, we note that our assumption of compositionality, i.e., that
 all casts can be decomposed into an upcast followed by a downcast, is