diff --git a/paper/gtt.tex b/paper/gtt.tex
index acdfbca6013120ed080b572966694805234a73b3..e1141d50804f5c79fcb6bd16dc7766d6a24c711c 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -6392,7 +6392,17 @@ introduction/elimination forms, and are all simple calculations.
     {\supcast{1}{1}[()]\ltdyn ()}
     \]
     Immediate by cast reduction.
-  \item TODO: $1$ elim
+  \item $1$ elim (continuations are terms case):
+    \[
+    \inferrule
+    {\supcast{1}{1}[\sem{V}] \ltdyn \sem{V'}[\sem\Phi]\\
+      \sem{M}[\sem\Psi] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]
+    }
+    {\pmpairWtoinZ {\sem V} {\sem{M}[\sem{\Psi}]}
+      \ltdyn
+      \dncast{\u B}{\u B'}[\pmpairWtoinZ {\sem V'[\sem\Phi]} {\sem{M'}[\sem{\Phi}]}]}
+    \]
+    which follows by identity expansion \ref{lem:ident-expansion}.
   \item $\times$ intro:
     \[
     \inferrule
@@ -6983,6 +6993,8 @@ some of the proofs simpler.
       \simpp{\absurd V} &=& \bindXtoYinZ {\simp V} x \absurd x\\
       \simpp{\caseofXthenYelseZ V {x_1. E_1}{x_2. E_2}} &=&
       \bindXtoYinZ {\simp V} x \caseofXthenYelseZ x {x_1. \simp {E_1}}{x_2. \simp {E_2}}\\
+      \simpp{\pmpairWtoinZ V {E}} &=&
+      \bindXtoYinZ V w {\pmpairWtoinZ w \simp {E}}\\
       \simpp{\pmpairWtoXYinZ V x y {E}} &=&
       \bindXtoYinZ V w {\pmpairWtoXYinZ w x y \simp {E}}\\
       \simpp{\pmmuXtoYinZ V x E} &=& \bindXtoYinZ {\simp V} y \pmmuXtoYinZ y x \simp{E}\\\\
@@ -6991,7 +7003,6 @@ some of the proofs simpler.
       \simpp{\inl V} &=& \bindXtoYinZ {\simp V} x \ret\inl x\\
       \simpp{\inr V} &=& \bindXtoYinZ {\simp V} x \ret\inr x\\
       \simp{()} &=& \ret ()\\
-      % TODO: 1 elim?
       \simp{(V_1,V_2)} &=& \bindXtoYinZ {\simp {V_1}}{x_1} \bindXtoYinZ {\simp {V_2}} {x_2} \ret (x_1,x_2)\\
       \simpp{\thunk M} &=& \ret \thunk \simp M\\
       \simpp{\roll V} &=& \bindXtoYinZ {\simp V} x \roll x\\
@@ -7205,8 +7216,14 @@ bigger thunkables from smaller ones.
       &\equidyn \pmpairWtoXYinZ V x y \bindXtoYinZ M z \ret\thunk\ret z\tag{$M$ thunkable}\\
       &\equidyn \bindXtoYinZ {(\pmpairWtoXYinZ V x y M)} z \ret\thunk\ret z\tag{commuting conversion}
     \end{align*}
-  \item $1$ elim TODO?
-  \item $\mu$ elim
+  \item $1$ elim
+    \begin{align*}
+      &\ret\thunk (\pmpairWtoinZ V x y M)\\
+      &\equidyn \pmpairWtoinZ V \ret\thunk \pmpairWtoinZ {()} M\tag{$1\eta$}\\
+      &\equidyn \pmpairWtoinZ V \ret\thunk M\tag{$1\beta$}\\
+      &\equidyn \pmpairWtoinZ V \bindXtoYinZ M z \ret\thunk\ret z\tag{$M$ thunkable}\\
+      &\equidyn \bindXtoYinZ {(\pmpairWtoinZ V M)} z \ret\thunk\ret z\tag{commuting conversion}
+    \end{align*}  \item $\mu$ elim
     \begin{align*}
       &\ret\thunk (\pmmuXtoYinZ V x M)\\
       &\equidyn \pmmuXtoYinZ V x \ret\thunk \pmmuXtoYinZ {\roll x} x M\tag{$\mu\eta$}\\