diff --git a/paper/gtt.tex b/paper/gtt.tex
index fe2676cc16a7403ba115d3756895b2664e26ac3f..acd1c4784ae8effc8dd9205d00bf6057bd4b3feb 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -116,6 +116,8 @@
 \newcommand{\cbpv}{\text{CBPV}_{\mu,\nu,\err,\ltdyn}}
 \newcommand{\cbpvtxt}{$\cbpv$}
 \newcommand{\sem}[1]{\llbracket#1\rrbracket}
+\newcommand{\sdncast}[2]{\sem{\dncast{#1}{#2}}}
+\newcommand{\supcast}[2]{\sem{\upcast{#1}{#2}}}
 \newcommand{\srho}[1]{\sem{#1}_\rho}
 \newcommand{\sdn}[2]{\srho{\dncast{#1}{#2}}}
 \newcommand{\hetplug}[1]{\langle#1\rangle}
@@ -204,6 +206,10 @@
 \newcommand{\kw}[1]{\texttt{#1}\,\,}
 \newcommand{\absurd}{\kw{absurd}}
 \newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
+\newcommand{\caseofX}[1]{\case #1}
+\newcommand{\thenY}{\{}
+\newcommand{\elseZ}[1]{\pipe #1 \}}
+
 \newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1\,\kw{to} (#2,#3). #4}
 \newcommand{\pmpairWtoinZ}[2]{\kw{split} #1\,\kw{to} (). #2}
 \newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \,\kw{to} \roll #2. #3}
@@ -1843,6 +1849,110 @@ is our graduality theorem.
   \end{mathpar}
 \end{theorem}
 
+Quite frequently we need the following commuting conversions, which
+are derivable from the $\eta$ rules for positive connectives.
+
+We need two versions of each rule for the positive value type
+connectives because of complex values: one when the continuation is a
+value and one when the continuation is a term.
+\begin{lemma}[Commuting Conversions]
+  All of the following are provable when both sides are well-typed/scoped:
+  % + 1 x F
+  \begin{mathpar}
+    E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]
+    \equidyn
+    \caseofXthenYelseZ V {x_1.E[V_1/y]}{x_2.E[V_2/y]}
+
+    S[\caseofXthenYelseZ V {x_1.M_1}{x_2.M_2}/y]
+    \equidyn
+    \caseofXthenYelseZ V {x_1.S[M_1/y]}{x_2.S[M_2/y]}
+
+    E[\pmpairWtoXYinZ V {x}{y} V']
+    \equidyn
+    \pmpairWtoXYinZ V {x}{y} E[V']
+
+    S[\pmpairWtoXYinZ V {x}{y} M']
+    \equidyn
+    \pmpairWtoXYinZ V {x}{y} S[M']
+
+    S[\bindXtoYinZ M x N]
+    \equidyn
+    \bindXtoYinZ M x S[N]
+  \end{mathpar}
+\end{lemma}
+\begin{proof}
+  \begin{enumerate}
+  \item For $+$, we just show one case since the other is exactly the same:
+    \begin{align*}
+      &E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]\\
+      &\equidyn
+      \caseofXthenYelseZ V {x_1'. E[\caseofXthenYelseZ {\inl x_1'} {x_1.V_1}{x_2.V_2}/y]}{x_2'. E[\caseofXthenYelseZ {\inr x_2'} {x_1.V_1}{x_2.V_2}/y]}\tag{$+\eta$}\\
+      &\equidyn \caseofXthenYelseZ V {x_1'. E[V_1[x_1'/x_1]]} {x_2'. E[V_2[x_2'/x_2]]}\tag{$+\beta$ twice}\\
+      &\equidyn \caseofXthenYelseZ V {x_1. E[V_1]} {x_2. E[V_2]} \tag{$\alpha$}
+    \end{align*}
+  \item For $\times$
+    \begin{align*}
+      &E[\pmpairWtoXYinZ V x y V']\\
+      &\pmpairWtoXYinZ V {x'}{y'} E[\pmpairWtoXYinZ {(x',y')} x y V']\tag{$\times\eta$}\\
+      &\pmpairWtoXYinZ V {x'}{y'} E[V'[x'/x][y'/y]] \tag{$\times\beta$}\\
+      &\pmpairWtoXYinZ V {x}{y} E[V'] \tag{$\alpha$}
+    \end{align*}
+  \item For $\u F$
+    \begin{align*}
+      &S[\bindXtoYinZ M x N]\\
+      &\bindXtoYinZ M y S[\bindXtoYinZ {\ret y} x N]\tag{$\u F\eta$}\\
+      &\bindXtoYinZ M y S[N[y/x]]\tag{$\u F\beta$}\\
+      &\bindXtoYinZ M y S[N] \tag{$\alpha$}
+    \end{align*}
+  \end{enumerate}
+\end{proof}
+
+\begin{lemma}{Cast Reductions}
+  The following are all provable
+  \begin{mathpar}
+    \sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inl V] \equidyn
+    \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{\upcast{A_1+A_2}{A_1'+A_2'}}[\inl V] \equidyn \inl \sem{\upcast{A_1}{A_1'}}[V]\\
+    
+    \sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inr V] \equidyn \inr \sem{\upcast{A_2}{A_2'}}[V]\\
+
+    \sem{\dncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}}[\ret (V_1,V_2)] \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)\\
+
+    \supcast{A_1\times A_2}{A_1'\times A_2'}[(V_1,V_2)] \equidyn (\supcast{A_1}{A_1'}[V_1], \supcast{A_2}{A_2'}[V_2])\\
+
+    (\sdncast{A \to \u B}{A' \to \u B'} M)\, V \equidyn
+    (\sdncast{\u B}{\u B'} M)\, (\supcast{A}{A'}{V})\\
+
+    (\force (\supcast{U(A\to\u B)}{U(A'\to\u B')} V))\,V' \equidyn
+    \bindXtoYinZ {\dncast{\u FA}{\u FA'}[\ret V']} x {\force (\supcast{U\u B}{U\u B'}{(\thunk (\force V\, x))})}\\
+
+    \pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
+    \sdncast{\u B_1}{\u B_1'} \pi M\\
+
+    \pi' \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
+    \sdncast{\u B_2}{\u B_2'} \pi' M\\
+
+    \pi \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
+    \equidyn
+    \force \supcast{U\u B_1}{U\u B_1'}{\thunk (\pi \force V)}\\
+
+    \pi' \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
+    \equidyn
+    \force \supcast{U\u B_2}{U\u B_2'}{\thunk (\pi' \force V)}\\
+
+    \sdncast{\u F U \u B}{\u F U \u B'}[\ret V] \equidyn \ret\thunk \sdncast{\u B}{\u B'}\force V\\
+
+    \force \supcast{U\u FA}{U \u F A'}[V]
+    \equidyn
+    \bindXtoYinZ {\force V} x \thunk\ret\upcast{A}{A'} x
+  \end{mathpar}
+\end{lemma}
+
 \begin{lemma}[Casts are EP Pairs]
   For any dynamic type interpretation,
   \begin{enumerate}
@@ -1858,8 +1968,63 @@ is our graduality theorem.
   By mutual induction on $A, \u B$
   \begin{enumerate}
   \item There's a few base cases about the dynamic type, then
-  \item $0$: TODO
-  \item $+$: TODO
+  \item $0$:
+    \begin{enumerate}
+    \item Retraction is
+      \[ x : 0 \vdash \ret x \equidyn \bindXtoYinZ {\ret\absurd x} y \err : \u F A \]
+      which holds by $0\eta$
+    \item Projection is
+      \[ \bullet : \u F A \vdash \bindXtoYinZ {(\bindXtoYinZ \bullet y \err)} x {\ret\absurd x} \ltdyn \bullet : \u F A \]
+      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 \err \tag{Strictness of Stacks}\\
+        &\ltdyn \bindXtoYinZ \bullet y \ret y \tag{$\err$ is $\bot$}\\
+        &\equidyn \bullet \tag{$\u F\eta$}
+      \end{align*}
+    \end{enumerate}
+  \item $+$:
+    \begin{enumerate}
+    \item Retraction is
+      \begin{align*}
+        &x : A_1 + A_2 \vdash\\
+        &\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \sem{\upcast{A_1+A_2}{A_1'+A_2'}}[x]]\\
+        &=\sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\caseofXthenYelseZ x {x_1. \inl\supcast{A_1}{A_1'}[x_1]}{x_1. \inr\supcast{A_2}{A_2'}[x_2]}]\\
+        &\equidyn
+        \caseofX x\tag{commuting conversion}\\
+        &\quad\thenY {x_1. \sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\inl\supcast{A_1}{A_1'}[x_1]]}\\
+        &\quad\elseZ {x_2. \sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}[\ret\inr\supcast{A_2}{A_2'}[x_2]]}\\
+        &\equidyn
+        \caseofX x\tag{cast computation}\\
+        &\quad\thenY{x_1. \bindXtoYinZ {\sdncast{\u F A_1}{\u F A_1'}[\ret \supcast{A_1}{A_1'}x_1]} {x_1} \ret \inl x_1}\\
+        &\quad\elseZ{x_2. \bindXtoYinZ {\sdncast{\u F A_2}{\u F A_2'}[\ret \supcast{A_2}{A_2'}x_2]} {x_2} \ret \inr x_2}\\
+        &\equidyn \caseofXthenYelseZ x {x_1. \ret \inl x_1} {x_2. \ret \inr x_2}\tag{IH retraction}\\
+        &\equidyn \ret x\tag{$+\eta$}
+      \end{align*}
+    \item For Projection:
+      \begin{align*}
+        &\bullet : A_1' + A_2' \vdash\\
+        &\bindXtoYinZ {\sdncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}} x \supcast{A_1+A_2}{A_1'+A_2'}[x]\\
+        &=
+        \bindXtoYinZ {(\bindXtoYinZ \bullet {x'} \caseofXthenYelseZ {x'} {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} \ret\inl x_1}{x_2'. \cdots})} x\\
+        &\quad\supcast{A_1+A_2}{A_1'+A_2'}\\
+        %%%%%%%%%%%%%%%
+        &\equidyn
+        \bindXtoYinZ \bullet x' \caseofX {x'} \tag{Commuting Conversion}\\
+        &\qquad \thenY {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} \supcast{A_1+A_2}{A_1'+A_2'}{\ret\inl x_1}}\\
+        &\qquad \elseZ {x_2'. \bindXtoYinZ {\sem{\dncast{\u FA_2}{\u FA_2'}}[\ret x_2']} {x_2} \supcast{A_1+A_2}{A_1'+A_2'}{\ret\inr x_2}}\\
+        %%%%%%%%%%%
+        &\equidyn
+        \bindXtoYinZ \bullet x' \caseofX {x'}\tag{Cast Computation}\\
+        &\qquad \thenY {x_1'. \bindXtoYinZ {\sem{\dncast{\u FA_1}{\u FA_1'}}[\ret x_1']} {x_1} {\ret\inl \supcast{A_1}{A_1'}x_1}}\\
+        &\qquad \elseZ {x_2'. \bindXtoYinZ {\sem{\dncast{\u FA_2}{\u FA_2'}}[\ret x_2']} {x_2} {\ret\inr \supcast{A_2}{A_2'}x_2}}\\
+        &\ltdyn
+        \bindXtoYinZ \bullet x' \caseofXthenYelseZ {x'} {x_1'. \ret\inl x_1'} {x_2'. \ret \inr x_2'}\tag{IH projection}\\
+        &\equidyn \bindXtoYinZ \bullet x' \ret x'\tag{$+\eta$}\\
+        &\equidyn \bullet \tag{$\u F\eta$}\\
+      \end{align*}
+    \end{enumerate}
   \item $1$: TODO
   \item $\times$: TODO
   \item $U$: By inductive hypothesis, $(x.\sem{\upcast{U\u B}{U\u
@@ -1871,24 +2036,24 @@ is our graduality theorem.
       \]
       Which we calculate as follows:
       \begin{align*}
-        \bindXtoYinZ {(\ret {\sem{\upcast{U\u B}{U \u B'}}})} y {\ret \thunk \sem{\dncast{\u B}{\u B'}}[\force y]}
-        &\equidyn {\ret \thunk \sem{\dncast{\u B}{\u B'}}[\force {\sem{\upcast{U\u B}{U \u B'}}}]}
-        \tag{$\u F\beta$}\\
-        &\equidyn \ret\thunk \force x \tag{IH computation Retraction}\\
+        &x : U\u B \vdash \\
+        &\sdncast{\u FU\u B}{\u FU\u B'}[{(\ret {\sem{\upcast{U\u B}{U \u B'}}[x]})}]\\
+        &\equidyn
+        \ret\thunk(\sdncast{\u B}{\u B'}[\force {\sem{\upcast{U\u B}{U \u B'}}}[x]])\tag{Cast Reduction}\\
+        &\equidyn \ret\thunk \force x \tag{IH Retraction}\\
         &\equidyn \ret x \tag{$U\eta$}
       \end{align*}
-    \item To show projection we need to prove:
-      \[
-      \bullet : \u F U \u B' \vdash \bindXtoYinZ {(\bindXtoYinZ \bullet y {\ret\thunk \sem{\dncast{\u B}{\u B'}}[\force y]})} x \ret \sem{\upcast{U \u B}{U \u B'}} \ltdyn \bullet : \u F U \u B'
-      \]
-      Which we calculate:
+    \item To show projection we calculate:
       \begin{align*}
-        \bindXtoYinZ {(\bindXtoYinZ \bullet y {\ret\thunk \sem{\dncast{\u B}{\u B'}}[\force y]})} x \ret \sem{\upcast{U \u B}{U \u B'}}
-        &\equidyn \bindXtoYinZ \bullet y \bindXtoYinZ {\ret\thunk \sem{\dncast{\u B}{\u B'}}[\force y]} x \ret \sem{\upcast{U \u B}{U \u B'}}
-        \tag{TODO: comm conv lemma $\u F\eta$}\\
-        &\equidyn \bindXtoYinZ \bullet y \ret \sem{\upcast{U \u B}{U \u B'}}[\thunk \sem{\dncast{\u B}{\u B'}}[\force y]] \tag{$\u F\beta$}\\
-        &\ltdyn \bindXtoYinZ \bullet y \ret y \tag{IH computation Projection}\\
-        &\equidyn \bullet \tag{$\u F \eta$}
+        &\bindXtoYinZ {\sdncast{\u FU\u B}{\u FU\u B'}[\bullet]} x \supcast{U\u B}{U\u B'}[x]\\
+        &\equidyn
+        \bindXtoYinZ \bullet {x'} \bindXtoYinZ {\sdncast{\u FU\u B}{\u FU\u B'}[\ret x']} x \supcast{U\u B}{U\u B'}[x]\tag{$\u F\eta$}\\
+        &\equidyn
+        \bindXtoYinZ \bullet {x'} \bindXtoYinZ {\ret\thunk(\sdncast{\u B}{\u B'}[\force x'])} x \supcast{U\u B}{U\u B'}[x]\tag{Cast Reduction}\\
+        &\equidyn
+        \bindXtoYinZ \bullet {x'} \supcast{U\u B}{U\u B'}[\thunk(\sdncast{\u B}{\u B'}[\force x'])] \tag{$\u F\beta$}\\
+        &\ltdyn \bindXtoYinZ \bullet {x'} x'\tag{IH Projection}\\
+        &\equidyn \bullet \tag{$\u F\eta$}
       \end{align*}
     \end{enumerate}
   \end{enumerate}
@@ -1909,7 +2074,7 @@ is our graduality theorem.
       \]
       We calculate:
       \begin{align*}
-        \sem{\dncast{\u F A}{\u F A'}}[\force \thunk (\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]
+        &\sem{\dncast{\u F A}{\u F A'}}[\force \thunk (\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]\\
         &\equidyn
         \sem{\dncast{\u F A}{\u F A'}}[(\bindXtoYinZ {\force z} x \ret \sem{\upcast{A}{A'}})]\tag{$U\beta$}\\
         &\equidyn
@@ -1921,12 +2086,18 @@ is our graduality theorem.
     \item To show projection we need to show
       \[
       w : U \u F A' \vdash
-      TODO
+      \thunk {(\bindXtoYinZ {\force {\thunk \sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})}
       \ltdyn w : U \u B'
       \]
+      We calculate as follows
+      \begin{align*}
+        &\thunk {(\bindXtoYinZ {\force {\thunk \sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})}\\
+        &\equidyn\thunk {(\bindXtoYinZ {{\sem{\dncast{\u F A}{\u F A'}}[\force w]}} x \ret \sem{\upcast{A}{A'}})} \tag{$U\beta$}\\
+        &\ltdyn \thunk {\force w} \tag{IH value projection}\\
+        & \equidyn w \tag{$U\eta$}
+      \end{align*}
     \end{enumerate}
   \end{enumerate}
-  TODO: tedious
 \end{proof}
 
 \begin{corollary}[Hom-set formulation of EP Pairs]
@@ -1962,6 +2133,7 @@ embeddings but I don't see anywhere where we need that.
   $(V_e, S_1)$ and $(V_e, S_2)$ are both value ep pairs, then
   \[ S_1 \equidyn S_2 \]
 \end{lemma}
+
 \begin{proof}
   By symmetry it is sufficient to show $S_1 \ltdyn S_2$.