diff --git a/paper/gtt.tex b/paper/gtt.tex
index c0549c3b1d33b5d1261cd62cb2db4dbdd4149e13..c98b92b6cc4dfde588691a1b48a4e4752bdfb2b2 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -7019,7 +7019,7 @@ $x$ exactly once, first, these two are the same.
   \]
 \end{definition}
 Thunkability/linearity of the translations of complex values/stacks are
-useed to prove the preservation of the $\eta$ principles for positive
+used to prove the preservation of the $\eta$ principles for positive
 types and the strictness of complex stacks with respect to errors under
 decomplexification.
 
@@ -7303,6 +7303,10 @@ morphisms from smaller ones.
   \end{enumerate}
 \end{longproof}
 
+Composing this with the previous translation from GTT to \cbpvstar\/
+shows that \emph{GTT value type upcasts are thunkable and computation
+  type downcasts are linear}.
+
 \begin{longonly}
   
 Since the translation takes values and stacks to terms, it cannot