diff --git a/paper/gtt.tex b/paper/gtt.tex
index fdb8face946cff536613772dc1501282cfa2a1df..e14ed2cfffd23154c7dc28648cc31da41d28de62 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -9380,6 +9380,27 @@ language, the $\eta$ principles do hold and so it must be graduality
 that fails, which corresponds to their failure of meaning
 preservation.
 
+Henglein's work on dynamic typing also uses an axiomatic semantics of
+casts, but axiomatizes behavior of casts at each type directly whereas
+we give a uniform definition of all casts and derive implementations
+for each type \cite{henglein94:dynamic-typing}.
+%
+Because of this, the theorems proven in that paper are more closely
+related to our model construction in section
+\secref{sec:contract-models}.
+%
+More specifically, many of the lemmas proven in the extended version
+of the paper have direct analogues in Henglein's work.
+%
+We have not included these lemmas in the paper because they are quite
+similar to lemmas proven in \citet{newahmed18}, and see there for a
+more detailed comparison.
+%
+Finally, we note that our assumption of compositionality, i.e., that
+all casts can be decomposed into an upcast followed by a downcast, is
+based on Henglein's analysis, where it was proven to hold in his
+coercion calculus.
+
 \iflong
 \paragraph{Gradual Typing Frameworks}
 \fi
@@ -9400,8 +9421,9 @@ statically typed language, whereas our approach is to ``gradualize''
 the axiomatic semantics of the typed language.
 %
 This means our approach accomplishes something quite different: their
-frameworks produce specific implementations, whereas our approach is
-about finding commonalities across different implementations.  
+frameworks produce specific implementations, whereas GTT (without
+$\eta$ principles) axiomatizes the commonalities across different
+implementations.
 % AA: Perhaps the above point should also be made in the intro. 
 Furthermore, while both the AGT and Gradualizer approaches prove various
 gradual typing correctness theorems by construction (gradual type