diff --git a/paper/gtt.tex b/paper/gtt.tex
index 4259e882c6d309a4543375cb853da3428773a1af..a64ce7918d39bb0a95f602696b8348f067af29fd 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -4782,7 +4782,7 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
   \inferrule
   {\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
     \Gamma \pipe \Delta \vdash M_{\u F} : \u F \dynv}
-  {\Gamma \pipe \Delta \vdash \dyncocaseFunF{M_{\to}}{M_{\u F}} : \u B}\\
+  {\Gamma \pipe \Delta \vdash \dyncocaseFunF{M_{\to}}{M_{\u F}} : \dync}\\
 
   \begin{longonly}
   \dncast{\u G}{\dync}\dyncocaseFunF{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)
@@ -5244,7 +5244,7 @@ the left-hand theorem would require more thunks/forces.
   $\supcast{A}{A'}$ is the identity and
   $\supcast{A'}{A''}\supcast{A}{A'}$ is $\supcast{A}{A''}$, and
   similarly for downcasts.  All of these properties are theorems in GTT
-  (Section~\ref{sec:theorem-in-gtt}), and the extened version in the
+  (Section~\ref{sec:theorems-in-gtt}), and the extened version in the
   supplementary materials shows that it takes quite a bit of work to prove
   them true in the model, which illustrates that the axiomatic theory of
   GTT encodes a lot of information with relatively few rules.