diff --git a/paper/gtt.tex b/paper/gtt.tex
index 2f25b347ab70a9477cdde6e8e02d7664dee61336..0fd64e7c4a5a812e2ff76648a4dc819e77c61d96 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -3993,7 +3993,6 @@ Theorem~\ref{thm:monadic-comonadic-casts} gives the result.
 %% section-retraction pair: i.e., that the downcast applied to the upcast
 %% is the identity.
 
-% TODO: can we take advantage of duality???
 %% With the large number of connectives comes a large number of proofs.
 %% %
 %% For each connective, we need four proofs: left and right rules for the
@@ -4325,6 +4324,12 @@ The easiest way to do this would be if for each $G$, we could rewrite
 $\dynv$ as a sum of the values that fit $G$ and those that don't:
 $\dynv \cong G + \dynv_{-G}$ because 
 
+\begin{lemma}[$\u F(+)$ Induction Principle]
+  $\Gamma\pipe \cdot : \u F (A_1 + A_2) \vdash M_1 \ltdyn M_2 : \u B$
+  holds if and only if
+  $\Gamma, V_1: A_1 \vdash M_1[\ret \inl V_1] \ltdyn M_2[\ret \inl V_2] : \u B$ and
+  $\Gamma, V_2: A_2 \vdash M_2[\ret \inr V_2] \ltdyn M_2[\ret \inr V_2] : \u B$ 
+\end{lemma}
 \begin{lemma}[Sum Injections are Value Embeddings]\label{lem:injections-are-embeddings}
   For any $A, A'$, there are value ep pairs from $A$ and $A'$ to
   $A+A'$ where the embeddings are $\inl$ and $\inr$.
@@ -4334,14 +4339,14 @@ $\dynv \cong G + \dynv_{-G}$ because
   projection to be $\bindXtoYinZ \bullet y \caseofXthenYelseZ y {\inl x. \ret
     x}{\inr _. \err}$.
   \begin{longonly}
-    This satisfies retraction:
+    This satisfies retraction (using $\u F(+)$ induction, $\inr$ case is the same):
     \begin{align*}
       \bindXtoYinZ {\inl x} y \caseofXthenYelseZ y {\inl x. \ret x}{\inr _. \err}
       &\equidyn \caseofXthenYelseZ {\inl x} {\inl x. \ret x}{\inr _. \err}\tag{$\u F\beta$}\\
       &\equidyn \ret x\tag{$+\beta$}
     \end{align*}
-    and projection:
-    \begin{align*} % TODO: fix this or make a lemma that says we don't need bullet
+    and projection (similarly using $\u F(+)$ induction):
+    \begin{align*}
       x': A+A'
       &\vdash \bindXtoYinZ x {(\bindXtoYinZ {\ret x'} y \caseofXthenYelseZ y {\inl x. \ret x}{\inr _. \err})} \ret \inl x\\
       &\equidyn \bindXtoYinZ x {(\caseofXthenYelseZ {x'} {\inl x. \ret x}{\inr _. \err})}\ret \inl x\tag{$\u F\beta$}\\
@@ -4570,6 +4575,7 @@ and representing sums as pairs, and lazy products as functions.
 The fact that isomorphisms are ep pairs is useful for constructing the
 ep pairs needed in the dynamic type interpretation.  
 \begin{lemma}[Isomorphisms are EP Pairs]
+  \label{lem:isos-are-ep}
   If $x:A \vdash V' : A'$ and $x':A' \vdash V : A$ are an isomorphism in
   that $V[V'/x'] \equidyn x$ and $V[V/x]\equidyn x'$, then $(x.V',
   \bindXtoYinZ \bullet {x'} \ret V')$ are a value ep pair from $A$ to
@@ -4861,7 +4867,7 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
     \[
     \upcast{\bool \times A}{A+A}V \equidyn \pmpairWtoXYinZ V {x}{y} \ifXthenYelseZ x {\inl y}{\inr y}
     \]
-    and the downcasts are given by lemma (TODO: some lemma about equidynamism isos)
+    and the downcasts are given by lemma \ref{lem:isos-are-ep}.
   \end{theorem}
   \begin{theorem}[Lazy Product to Tag Checking Function]
     In Scheme-like GTT, we can prove
@@ -4870,7 +4876,7 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
     \equidyn
     \lambda x:\bool. \ifXthenYelseZ x {\pi \bullet}{\pi' \bullet}
     \]
-    and the upcasts are given by lemma (TODO)
+    and the upcasts are given by lemma \ref{lem:isos-are-ep}.
   \end{theorem}
 
   \begin{theorem}[Ground Mismatches are Errors]
@@ -4943,7 +4949,8 @@ interpretation.
       x : 1 \vdash \supcast{1}{1} &=& x\\
       \bullet : \u F 1 \vdash \sdncast{\u F1}{\u F1} &=& x\\
 \fi
-      x : \sem{A_1}\times\sem{A_2} \vdash \sem{\upcast{A_1\times A_2}{A_1'\times A_2'}} &=& \pmpairWtoXYinZ x {x_1}{x_2} (\supcast{A_1}{A_1'}[x_1], \supcast{A_2}{A_2'}[x_2])\\
+      x : \sem{A_1}\times\sem{A_2} \vdash \sem{\upcast{A_1\times A_2}{A_1'\times A_2'}} &=& \pmpairWtoXYinZ x {x_1}{x_2}\\
+      &&(\supcast{A_1}{A_1'}[x_1], \supcast{A_2}{A_2'}[x_2])\\
       \bullet \vdash \sdncast{\u F(A_1 \times A_2)}{\u F(A_1' \times A_2')}
       &=&
       \bindXtoYinZ \bullet {x'} \pmpairWtoXYinZ {x'} {x_1'}{x_2'}\\
@@ -5079,6 +5086,7 @@ Figure~\ref{fig:normalized}.
 \end{figure}
 
 \begin{lemma}[Normalized Type Dynamism is Equivalent to Original]
+  \label{lem:norm-type-dyn}
   $T \ltdyn T'$ is provable in the normalized typed dynamism
   definition iff it is provable in the original typed
   dynamism definition.
@@ -5279,6 +5287,8 @@ the left-hand theorem would require more thunks/forces.
     \bindXtoYinZ {\sem{\dncast{A_1}{A_1'}}[\ret V]} {x_1} \ret \inl x_1\\
     &\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inr V] \equidyn
     \bindXtoYinZ {\sem{\dncast{A_2}{A_2'}}[\ret V]} {x_2} \ret \inr x_2\\
+    &\sem{\dncast{\u F 1}{\u F1}} \equidyn \bullet\\
+    &\sem{\upcast{ 1}{1}}[x] \equidyn x\\
     &\sem{\dncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}}[\ret (V_1,V_2)]\\
     &\quad\equidyn
     \bindXtoYinZ {\sdncast{\u FA_1}{\u F A_1'}[\ret V_1]} {x_1} \bindXtoYinZ {\sdncast{\u FA_2}{\u F A_2'}[\ret V_2]} {x_2} \ret (x_1,x_2)\\
@@ -5311,6 +5321,7 @@ are ep pairs.  Before doing so, we prove the following lemma, which is
 used for transitivity (e.g. in the $A \ltdyn \dynv$ rule, which uses a
 composition $A \ltdyn \floor{A} \ltdyn \dynv$):
 \begin{lemma}[EP Pairs Compose]
+  \label{lem:ep-pairs-compose}
   \begin{enumerate}
   \item If $(V_1, S_1)$ is a value ep pair from $A_1$ to $A_2$ and
     $(V_2,S_2)$ is a value ep pair from $A_2$ to $A_3$, then
@@ -5346,6 +5357,12 @@ composition $A \ltdyn \floor{A} \ltdyn \dynv$):
     \end{align*}
   \end{enumerate}
 \end{longproof}
+\begin{longonly}
+\begin{lemma}[Identity EP Pair]
+  \label{ep-pair-id}
+  $(x. x, \bullet)$ is an ep pair (value or computation).
+\end{lemma}  
+\end{longonly}
 
 Now, we show that all casts are ep pairs.
 %
@@ -5365,7 +5382,7 @@ The proof is a somewhat tedious, but straightforward calculation.
 \begin{longproof}
   By induction on normalized type dynamism derivations.
   \begin{enumerate}
-  \item TODO: There's a few base cases about the dynamic type
+  \item $A \ltdyn A$ ($A \in \{\dyn, 1\}$), because identity is an ep pair.
   \item $0 \ltdyn A$ (that $A \in \{ \dyn, 0 \}$ is not important):
     \begin{enumerate}
     \item Retraction is
@@ -5376,7 +5393,7 @@ The proof is a somewhat tedious, but straightforward calculation.
       Which we calculate:
       \begin{align*}
         &\bindXtoYinZ {(\bindXtoYinZ \bullet y \err)} x {\ret\absurd x}\\
-        &\equidyn \bindXtoYinZ \bullet y \bindXtoYinZ \err x {\ret\absurd x}\tag{TODO comm conv}\\
+        &\equidyn \bindXtoYinZ \bullet y \bindXtoYinZ \err x {\ret\absurd x}\tag{comm conv}\\
         &\equidyn \bindXtoYinZ \bullet y \err \tag{Strictness of Stacks}\\
         &\ltdyn \bindXtoYinZ \bullet y \ret y \tag{$\err$ is $\bot$}\\
         &\equidyn \bullet \tag{$\u F\eta$}
@@ -5423,7 +5440,6 @@ The proof is a somewhat tedious, but straightforward calculation.
         &\equidyn \bullet \tag{$\u F\eta$}\\
       \end{align*}
     \end{enumerate}
-  \item $1$: TODO
   \item $\times$:
     \begin{enumerate}
     \item First, Retraction:
@@ -5701,7 +5717,7 @@ The proof is a somewhat tedious, but straightforward calculation.
         &\equidyn
         \sem{\dncast{\u F A}{\u F A'}}[(\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]\tag{$U\beta$}\\
         &\equidyn
-        \bindXtoYinZ {\force z} x \sem{\dncast{\u F A}{\u F A'}}[\ret \sem{\upcast{A}{A'}}] \tag{TODO: comm conv}\\
+        \bindXtoYinZ {\force z} x \sem{\dncast{\u F A}{\u F A'}}[\ret \sem{\upcast{A}{A'}}] \tag{comm conv}\\
         &\equidyn
         \bindXtoYinZ {\force z} x \ret x \tag{IH value retraction}\\
         &\equidyn \force z \tag{$\u F\eta$}        
@@ -5808,6 +5824,7 @@ axiomatic graduality theorem, and to prove a conservativity result,
 which says that a GTT homogeneous term dynamism is the same as a
 \cbpvstar\/ inequality between their translations.
 \begin{lemma}[Identity Expansion]
+  \label{lem:ident-expansion}
   For any $A$ and $\u B$,
   \begin{mathpar}
     x:A \vdash \sem{\upcast{A}{A}} \equidyn x : A\and
@@ -5816,16 +5833,17 @@ which says that a GTT homogeneous term dynamism is the same as a
 \end{lemma}
 \begin{proof}
   We proceed by induction on $A, \u B$, following the proof that
-  reflexivity is admissible given in (TODO: ref)
+  reflexivity is admissible given in \ref{lem:norm-type-dyn}.
   \begin{enumerate}
   \item If $A \in \{1, \dynv \}$, then $\supcast{A}{A}[x] = x$.
   \item If $A = 0$, then $\absurd x \equidyn x$ by $0\eta$.
   \item If $A = U \u B$, then by inductive hypothesis $\sdncast{\u
-    B}{\u B} \equidyn \bullet$. By lemma (TODO: ref), $(x. x,
-    \bullet)$ is a computation ep pair from $\u B$ to itself. But by
-    (TODO: ref), $(\supcast{U\u B}{U\u B}[x], \bullet)$ is also a
-    computation ep pair so the result follows by uniqueness of
-    embeddings from computation projections (TODO: ref).
+    B}{\u B} \equidyn \bullet$. By lemma \ref{ep-pair-id},
+    $(x. x, \bullet)$ is a computation ep pair from $\u B$ to
+    itself. But by \ref{lem:casts-are-ep-pairs}, $(\supcast{U\u
+      B}{U\u B}[x], \bullet)$ is also a computation ep pair so the
+    result follows by uniqueness of embeddings from computation
+    projections \ref{lem:adjoints-unique-cbpvstar}.
   \item If $A = A_1\times A_2$ or $A = A_1+A_2$, the result follows by
     the $\eta$ principle and inductive hypothesis.
   \item If $\u B = \dync$, $\sdncast{\dync}{\dync} = \bullet$.
@@ -5936,7 +5954,7 @@ use this lemma to translate \emph{transitivity} of term dynamism in GTT.
         \[  \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B''}] \equidyn \sdncast{\u B}{\u B''}\]
         so then both sides form ep pairs paired with $\sdncast{\u
           B}{\u B''}$, so it follows because computation projections
-        determine embeddings (TODO ref).
+        determine embeddings \ref{lem:adjoints-unique-cbpvstar}.
       \end{enumerate}
     \end{enumerate}
   \item $\u B \ltdyn \u B' \ltdyn \u B''$
@@ -6012,6 +6030,7 @@ These arise in the proof cases for return and thunk, because in those
 cases the inductive hypothesis is in terms of an upcast (downcast) and
 the conclusion is in terms of a a downcast (upcast).
 \begin{lemma}[Hom-set formulation of Adjunction]
+  \label{lem:hom-set-adj}
   For any value embedding-projection pair $V_e,S_p$ from $A$ to $A'$,
   the following are equivalent:
   \begin{small}
@@ -6094,7 +6113,8 @@ introduction/elimination forms, and are all simple calculations.
 \begin{longproof}
   By mutual induction over term dynamism derivations. For the $\beta,
   \eta$ and reflexivity rules, we use the identity expansion lemma and
-  the corresponding $\beta, \eta$ rule of \cbpvstar\  (TODO ref).
+  the corresponding $\beta, \eta$ rule of
+  \cbpvstar\ref{lem:ident-expansion}.
 
   For compatibility rules a pattern emerges.  Universal rules
   (positive intro, negative elim) are easy, we don't need to reason about
@@ -6315,7 +6335,7 @@ introduction/elimination forms, and are all simple calculations.
     identity casts are identities.
 
     %% Value Compat Rules
-  \item TODO: $0$ elim, we do the term case, the value case is similar
+  \item $0$ elim, we do the term case, the value case is similar
     \[
     \inferrule
     {\upcast{0}{0}[\sem{V}] \ltdyn \sem{V'}[\sem\Phi]}
@@ -6369,7 +6389,7 @@ introduction/elimination forms, and are all simple calculations.
     {}
     {\supcast{1}{1}[()]\ltdyn ()}
     \]
-    Immediate by cast reduction? TODO: figure out what we're doing with $1$.
+    Immediate by cast reduction.
   \item TODO: $1$ elim
   \item $\times$ intro:
     \[
@@ -6430,7 +6450,7 @@ introduction/elimination forms, and are all simple calculations.
     {\supcast{U \u B}{U \u B'}[\sem{V}] \ltdyn \sem{V'}[\sem\Phi]}
     {\force \sem V \ltdyn \sdncast{\u B}{\u B'}\force \sem {V'}[\sem\Phi]}
     \]
-    By hom-set formulation of adjunction (TODO: ref).
+    By hom-set formulation of adjunction \ref{lem:hom-set-adj}.
     %% Computation Compat Rules
   \item $\top$ intro:
     \[
@@ -6509,7 +6529,7 @@ introduction/elimination forms, and are all simple calculations.
     {\supcast{A}{A'}[\sem{V}] \ltdyn \sem{V'}[\sem{\Phi}]}
     {\ret\sem{V}\ltdyn \sdncast{\u F A}{\u FA'}[\ret\sem{V'}[\sem{\Phi}]]}
     \]
-    By hom-set definition of adjunction (TODO ref)
+    By hom-set definition of adjunction \ref{lem:hom-set-adj}
   \item We need to show
     \[
     \inferrule
@@ -7083,7 +7103,8 @@ First, the following lemma is useful for optimizing programs with
 thunkable subterms.
 Intuitively, since a thunkable has ``no effects'' it can be reorderd
 past any other effectful binding.
-Furhmann (TODO cite) calls a morphism that has this property \emph{central}.
+Furhmann \citep{fuhrmann1999direct} calls a morphism that has this
+property \emph{central}.
 \begin{lemma}[Thunkable are Central]
   If $\Gamma \vdash M : \u F A$ is thunkable and $\Gamma \vdash N : \u
   F A'$ and $\Gamma , x:A, y:A' \vdash N' : \u B$, then