diff --git a/paper/gtt.tex b/paper/gtt.tex
index 25c9867eeae025fc039bde0c7d8c0333f0c90c14..6fbc1935dbbdc4f2c4942e80c297b2aaa81426a9 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -2162,6 +2162,61 @@ which is true by downcast left.
 
 \subsection{Type-generic Properties of Casts}
 
+The specification of upcasts and downcasts by their right and left
+$\ltdyn$ rules defines them \emph{uniquely} up to $\equidyn$.
+%
+In category-theoretic terms this says that ``being an upcast/downcast''
+is a \emph{universal property}, and so we can show that something else
+is equivalent to the upcast or downcast by showing that it has the
+\emph{same} property.
+%
+
+\begin{theorem}[Specification for Casts is a Universal Property]
+  ~ \label{thm:casts-unique}
+  \begin{enumerate}
+  \item 
+  If $A \ltdyn A'$ and $x : A \vdash V : A'$ is a comples value such that
+  \begin{mathpar}
+    \inferrule
+    {}
+    {x : A \vdash x \ltdyn V : A \ltdyn A'}
+
+    \inferrule
+    {}
+    {x \ltdyn x' : A \ltdyn A' \vdash V \ltdyn x' : A'}
+  \end{mathpar}
+  then $x : A \vdash V \equidyn \upcast{A}{A'}{x} : A'$.
+
+  \item 
+  If $\u B \ltdyn \u B'$ and $\bullet' : \u B' \vdash S :
+  \u B$ is a complex stack such that
+  \begin{mathpar}
+    \inferrule
+    {}
+    {\bullet' : \u B' \vdash S \ltdyn \bullet' : \u B \ltdyn \u B'}
+
+    \inferrule
+    {}
+    {\bullet \ltdyn \bullet' : \u B \ltdyn \u B' \vdash \bullet \ltdyn S : \u B}
+  \end{mathpar}
+  then $\bullet' : \u B' \vdash S \equidyn \dncast{\u B}{\u B'}\bullet' : \u B$
+  \end{enumerate}
+\end{theorem}
+\begin{proof}
+  For the first part, to show $\upcast{A}{A'}{x} \ltdyn V$, by upcast
+  left, it suffices to show $x \ltdyn V : A \ltdyn A'$, which is one
+  assumption.  To show $V \ltdyn \upcast{A}{A'}{x}$, we substitute into
+  the second assumption with $x \ltdyn \upcast{A}{A'}{x} : A \ltdyn A'$,
+  which is true by upcast right.
+
+  For the second part, to show $S \ltdyn \dncast{\u B}{\u
+    B'}{\bullet'}$, by downcast right, it suffices to show $S \ltdyn
+  \bullet' : \u B \ltdyn \u B'$, which is one of the assumptions.  To
+  show $\dncast{\u B}{\u B'}{\bullet'} \ltdyn S$, we substitute into the
+  second assumption with $\dncast{\u B}{\u B'}{\bullet'} \ltdyn
+  \bullet'$, which is true by downcast left.
+\end{proof}
+
 The following results apply to casts in any types:
 
 \begin{theorem}[Casts (de)composition] \label{thm:decomposition}
@@ -2358,55 +2413,6 @@ for casts into the dynamic type.  More generally:
 \end{enumerate}
 \end{proof}
 
-The specification of upcasts and downcasts by their right and left
-$\ltdyn$ rules defines them \emph{uniquely} up to $\equidyn$.
-%
-In category-theoretic terms this says that ``being an upcast/downcast''
-is a \emph{universal property}, and so we can show that something else
-is equivalent to the upcast or downcast by showing that it has the
-\emph{same} property.
-%
-
-\begin{theorem}[Specification for Casts is a Universal Property]
-  ~ \label{thm:casts-unique}
-  \begin{enumerate}
-  \item 
-  If $A \ltdyn A'$ and $x : A \vdash V[x] : A'$ is a value such that
-  \begin{mathpar}
-    \inferrule
-    {}
-    {x : A \ltdyn x' : A' \vdash V[x] \ltdyn x' : A'}
-
-    \inferrule
-    {}
-    {x_2 : A \ltdyn x : A \vdash x_2 \ltdyn V[x] : A \ltdyn A'}
-  \end{mathpar}
-  then $x : A \vdash V \equidyn x : A$.
-
-  \item 
-  If $\u B \ltdyn \u B'$ and $\bullet : \u B' \vdash S :
-  \u B$ is a stack such that
-  \begin{mathpar}
-    \inferrule
-    {}
-    {\bullet \ltdyn \bullet : \u B' \vdash S \ltdyn \bullet : \u B \ltdyn \u B'}
-
-    \inferrule
-    {}
-    {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn S : \u B}
-  \end{mathpar}
-  then $\bullet : \u B' \vdash S \equidyn \dncast{\u B}{\u B'}\bullet : \u B$
-  \end{enumerate}
-\end{theorem}
-\begin{proof}
-  \begin{mathpar}
-    \inferrule*[right=substitution]
-    {x_1 \ltdyn x_2 \vdash x_1 \ltdyn \upcast{A}{A'}x_2 : A \ltdyn A' \and x_1 \ltdyn x_2' : A \ltdyn A' \vdash V_u[x_1] \ltdyn x_2' : A'}
-    {x_1 : A \ltdyn x_2 : A \vdash V_u[x_1] \ltdyn \upcast{A}{A'} x_2 : A'}
-  \end{mathpar}
-  The other direction is essentially the same, but swapping $V_u$ and
-  the upcast. FIXME: todo
-\end{proof}
 
 \subsection{Implementation of Casts}