diff --git a/paper/gtt.tex b/paper/gtt.tex
index 82b67e2de63bc579b8d3e88e2fcecbe31de41b71..6f1c339d93d2c5fa0d7512434f2e65ff361a0262 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1196,7 +1196,8 @@ TODO: do we actually know what would go wrong in that case?
     {\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
     {\Gamma \mid \Delta \vdash \pi' M : \u B_2}
   \end{mathpar}
-  \caption{GTT Type Dynamism, Dynamism Contexts, and Terms}
+\caption{GTT Type Dynamism, Dynamism Contexts, and Terms}
+\label{fig:gtt-type-dynamism-and-terms}
 \end{small}
 \end{figure}
 
@@ -3162,6 +3163,57 @@ characterization of the casts for the monad/comonad of $F \dashv U$:
 
 \subsection{Upcasts are Values, Downcasts are Stacks}
 
+\begin{definition}[Ground types]
+  A \emph{ground type} is generated by the following grammar:
+  \[
+  \begin{array}{rcl}
+    G & ::= & 1 \mid \dynv \times \dynv \mid 0 \mid \dynv + \dynv \mid U \dync\\
+    \u G & ::= & \top \mid \dync \with \dync \mid \dynv \to \dync \mid \u F \dynv
+  \end{array}
+  \]
+\end{definition}
+
+\begin{definition}[Ground type precision]
+  Let $A \ltdyn' A'$ and $\u B \ltdyn' \u B'$ be the relations defined
+  by the rules in Figure~\ref{fig:gtt-type-dynamism-and-terms}
+  with the axioms $A \ltdyn \dynv$ and $\u B \ltdyn \dync$ restricted to
+  ground types---i.e., replaced by $G \ltdyn \dynv$ and $\u G \ltdyn \dync$.
+\end{definition}
+
+\begin{lemma} \label{lem:find-ground-type}
+  For any type $A$, there exists a ground type $G$ with $A \ltdyn' G$.
+  For any type $\u B$, there exists a ground type $\u G$ with $\u B
+  \ltdyn' \u G$.
+\end{lemma}
+\begin{proof}
+By induction on the type.  For example, in the case for $A_1 + A_2$, we
+have by the inductive hypothesis $A_1 \ltdyn' G_1$ and $A_2 \ltdyn'
+G_2$, so $A_1 \ltdyn' G_1' \ltdyn' \dynv$ and $A_2 \ltdyn' G_2 \ltdyn'
+\dynv$ by transitivity, so $A_1 + A_2 \ltdyn' \dynv + \dynv$ by
+congruence, which is ground.  In the case for $\u F A$, we have $A
+\ltdyn G$ by the inductive hypothesis, so $A \ltdyn' \dynv$ by
+transitivity, so $\u F A \ltdyn \u F \dynv$ by congruence, which is
+ground.
+\end{proof}
+
+\begin{lemma}[Alternative Characterization of Type Precision]
+  $A \ltdyn A'$ iff $A \ltdyn' A'$ and $\u B \ltdyn \u B'$ iff $\u B
+  \ltdyn' \u B'$
+\end{lemma}
+
+\begin{proof}
+The ``if'' direction is immediate by induction because every rule of
+$\ltdyn'$ is a rule of $\ltdyn$.  To show $\ltdyn$ is contained in
+$\ltdyn'$, we do induction on the derivation of $\ltdyn$, where every
+rule is true for $\ltdyn'$, except $A \ltdyn \dynv$ and $\u B \ltdyn
+\dync$.  For these, we use Lemma~\ref{lem:find-ground-type} to find
+ground types $G$ and $\u G$ such that $A \ltdyn G$ and $\u B \ltdyn \u
+G$, and then use transitivity with $G \ltdyn \dynv$ and $\u G \ltdyn
+\dync$.
+\end{proof}
+
+
+
 \begin{theorem}{Upcasts are (Complex) Values, Downcasts are (Complex) Stacks}
   If the tagging upcasts are complex values and untagging downcasts
   are stacks, then all upcasts are complex values and all downcasts