diff --git a/paper/gtt.tex b/paper/gtt.tex
index cca4317669a07f899ae94a61d8fa3401333a720c..167d630a272a5f3dd256f1adbe9cbb764c1718bc 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -3485,7 +3485,28 @@ morphisms from smaller ones.
   If $E \ltdyn E'$ then $\simp E \ltdyn \simp{E'} in simple CBPV$
 \end{theorem}
 \begin{proof}
-  ...
+  $\beta$ axioms need to reduce administrative redices ugh
+  \begin{enumerate}
+  \item TODO: $\beta, \eta$ axioms (Value $\beta$ principles have
+    admin redexes, Value $\eta$?, Comp $\eta$ involve stacks, Comp
+    $\beta$ are probably trivial)
+  \item All compatibility rules are translated to compatibility rules
+    in simple CBPV, usually using an $\u F$-binding.
+  \item Substitution axioms
+  \item Stack axioms
+    We need to show for $S$ a complex stack,
+    that
+    \[ \sem{S[\err]} \equidyn \err \]
+    By stack compositionality we know
+    \[ \sem{S[\err]} \equidyn \sem{S[\force z]}[{\thunk \err/z}] \]
+    \begin{align*}
+      \sem{S[\force z]}[{\thunk \err/z}]
+      &\equidyn \sem{S[\force z]}[\thunk {(\bindXtoYinZ \err y \err)}/z]\tag{Stacks preserve $\err$}\\
+      &\equidyn
+      \bindXtoYinZ \err y \sem{S[\force z]}[{\thunk \err/z}] \tag{$S[\force z]$ is linear in $z$}\\
+      &\equidyn \err \tag{Stacks preserve $\err$}
+    \end{align*}
+  \end{enumerate}
 \end{proof}
 
 \begin{lemma}[De-complexification is equivalent to Identity]