diff --git a/paper/gtt.tex b/paper/gtt.tex
index 2bec03b826c4254c47c175413c84be2d841b4462..6b645f7d326f84d4e3d5426259abdb817b21fa55 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -9150,24 +9150,6 @@ arguments on the stack.
 
 \bibliography{max}
 
-\appendix
-
-\section{Program Equivalences and Inequivalences in Previous Work}
-
-We should show here what fails in eager and transient semantics.
-
-In this appendix we present for the reader who is unfamiliar with
-call-by-push-value two type theories for call-by-value and
-call-by-name gradual typing in this style.
-%
-In each we prove one of the non-obvious uniqueness theorems that we
-showed for CBPV: in CBV we show the function type must be the
-thunkable, wrapping implementation and for the CBN what would we do??
-
-\section{Mini Call-by-value Gradual Type Theory}
-
-\section{Mini Call-by-name Gradual Type Theory}
-
 \end{document}
 
 %% Local Variables: