diff --git a/paper/gtt.tex b/paper/gtt.tex
index 3de945b949e422666f4c656560189c2eb0e09c41..15459fe4ea0a2041dcd79b4c0f2658f79acc6f4f 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -238,7 +238,7 @@
 
 \begin{abstract}
   Gradually typed languages are designed to support both dynamically
-  typed and statically typed programming styles that preserves the
+  typed and statically typed programming styles and preserve the
   benefits of each: dynamic code can be used without conforming to the
   syntactic type discipline, and static code provides sound reasoning
   principles that formally justify type-based refactorings and
@@ -290,7 +290,7 @@
   equivalent to the ``wrapping'' semantics, and any system that
   differs from it must violate graduality or extensionality (typically
   the latter), extending a previous result for a fragment of
-  call-by-name to full call-by-value and call-by-name.
+  call-by-name to full call-by-name and call-by-value.
   %
   On the other hand the structure of the dynamic type itself, which is
   taken for granted to be a sum in previous work, is not uniquely
@@ -430,12 +430,12 @@ theory or metric spaces for denotational semantics.
 These semantic techniques are essential, but obscure the basic
 principles being studied due to heavy formal machinery.
 
-Instead, we will study program equivalence properpties of gradual
+Instead, we will study program equivalence properties of gradual
 typing via \emph{axiomatic semantics}.
 %
 This has the benefit that equivalence and approximation properties can
 be stated and proven entirely syntactically, and allows for multiple
-different concrete interpertations using logical relations, domains,
+different concrete interpretations using logical relations, domains,
 etc.
 %
 This way we can add gradual typing as a sort of ``axiomatic mixin''
@@ -1953,19 +1953,19 @@ 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
+  % TODO: 1, 0?
   \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]
+    S[\caseofXthenYelseZ V {x_1.M_1}{x_2.M_2}]
     \equidyn
-    \caseofXthenYelseZ V {x_1.S[M_1/y]}{x_2.S[M_2/y]}
+    \caseofXthenYelseZ V {x_1.S[M_1]}{x_2.S[M_2]}
 
-    E[\pmpairWtoXYinZ V {x}{y} V']
+    E[\pmpairWtoXYinZ V {x}{y} V'/z]
     \equidyn
-    \pmpairWtoXYinZ V {x}{y} E[V']
+    \pmpairWtoXYinZ V {x}{y} E[V'/z]
 
     S[\pmpairWtoXYinZ V {x}{y} M']
     \equidyn
@@ -3180,7 +3180,7 @@ The following lemma is key to proving the coherence lemma.
   \caption{Contract Translation of casts}
 \end{figure}
 
-\subsection{Complex Value/Stack Elimination}
+\section{Complex Value/Stack Elimination}
 
 Next, to bridge the gap between the semantic notion of complex value
 and stack with the more rigid operational notion, we perform a
@@ -3226,9 +3226,12 @@ variable $x$ of type $U\u B$ ``always forces $x$ when forced'':
   \begin{mathpar}
     \begin{array}{rcl}
       \simp {\ret V} &= & \bindXtoYinZ {\simp V} x \ret x\\
-      \simp {M\, V}  &=& \bindXtoYinZ {\simp V} x \simp M\, x\\\\
+      \simpp {M\, V}  &=& \bindXtoYinZ {\simp V} x \simp M\, x\\
+      \simpp{\force V} &=& \bindXtoYinZ {\simp V} x \force x\\
 
       % Values: 0, +, 1, x, U, mu
+      \simp x &=& \ret x\\
+      \simpp{\absurd V} &=& \bindXtoYinZ {\simp V} x \absurd x\\
       \simpp{\inl V} &=& \bindXtoYinZ {\simp V} x \ret\inl x\\
       \simpp{\inr V} &=& \bindXtoYinZ {\simp V} x \ret\inr x\\
       \simpp{\caseofXthenYelseZ V {x_1. V_1}{x_2. V_2}} &=&
@@ -3244,11 +3247,45 @@ variable $x$ of type $U\u B$ ``always forces $x$ when forced'':
     \end{array}
   \end{mathpar}
 \end{definition}
+
 \begin{lemma}[De-complexification De-complexifies]
   For any well-typed $M, V$, $\simp M$ and $\simp V$ only use pattern
   matching into terms.
 \end{lemma}
 
+We need a few lemmas about thunkables and linears to prove that
+complex values become thunkable and complex stacks become linear.
+
+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}.
+\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
+  \[
+  \bindXtoYinZ M x \bindXtoYinZ N y N'
+  \equidyn
+ \bindXtoYinZ N y \bindXtoYinZ M x N'
+  \]
+\end{lemma}
+\begin{proof}
+  \begin{align*}
+    &\bindXtoYinZ M x \bindXtoYinZ N y N'\\
+    &\equidyn
+    \bindXtoYinZ M x \bindXtoYinZ N y \bindXtoYinZ {\force \thunk \ret x} x N' \tag{$U\beta,\u F\beta$}\\
+    &\equidyn\bindXtoYinZ M x \bindXtoYinZ {\ret\thunk\ret x} w \bindXtoYinZ N y \bindXtoYinZ {\force w} x N' \tag{$\u F\beta$}\\
+    &\equidyn\bindXtoYinZ {(\bindXtoYinZ M x {\ret\thunk\ret x})} w \bindXtoYinZ N y \bindXtoYinZ {\force w} x N' \tag{$\u F\eta$}\\
+    &\equidyn\bindXtoYinZ {\ret \thunk M} w \bindXtoYinZ N y \bindXtoYinZ {\force w} x N' \tag{$M$ thunkable}\\    
+    &\equidyn\bindXtoYinZ N y \bindXtoYinZ {\force \thunk M} x N' \tag{$\u F\beta$}\\
+    &\equidyn\bindXtoYinZ N y \bindXtoYinZ M x N' \tag{$U\beta$}\\    
+  \end{align*}
+\end{proof}
+
+Next, we show thunkables are closed under composition and that return
+of a value is always thunkable.  This allows us to easily build up
+bigger thunkables from smaller ones.
 \begin{lemma}[Thunkables compose]
   If $\Gamma \vdash M : \u F A$ and $\Gamma, x : A \vdash N : \u F A'$
   are thunkable, then
@@ -3258,14 +3295,14 @@ variable $x$ of type $U\u B$ ``always forces $x$ when forced'':
 \begin{proof}
   \begin{align*}
     &\bindXtoYinZ {(\bindXtoYinZ M x N)} y \ret\thunk\ret y\\
-    &\equidyn \bindXtoYinZ M x \bindXtoYinZ N y \ret\thunk\ret y\\
-    &\equidyn \bindXtoYinZ M x \ret \thunk N \\
-    &\equidyn \bindXtoYinZ M x \ret \thunk (\bindXtoYinZ {\ret x} x N)\\
-    &\equidyn \bindXtoYinZ M x \bindXtoYinZ {\ret\thunk\ret x} w \ret \thunk (\bindXtoYinZ {\force w} x N)\\
-    &\equidyn \bindXtoYinZ {(\bindXtoYinZ M x \ret\thunk\ret x)} w \ret \thunk (\bindXtoYinZ {\force w} x N)\\
-    &\equidyn \bindXtoYinZ {\ret\thunk M} w \ret \thunk (\bindXtoYinZ {\force w} x N)\\
-    &\equidyn  \ret \thunk (\bindXtoYinZ {\force \thunk M} x N)\\
-    &\equidyn  \ret \thunk (\bindXtoYinZ {M} x N)\\
+    &\equidyn \bindXtoYinZ M x \bindXtoYinZ N y \ret\thunk\ret y\tag{$\u F\eta$}\\
+    &\equidyn \bindXtoYinZ M x \ret \thunk N \tag{$N$ thunkable}\\
+    &\equidyn \bindXtoYinZ M x \ret \thunk (\bindXtoYinZ {\ret x} x N)\tag{$\u F\beta$}\\
+    &\equidyn \bindXtoYinZ M x \bindXtoYinZ {\ret\thunk\ret x} w \ret \thunk (\bindXtoYinZ {\force w} x N)\tag{$\u F\beta,U\beta$}\\
+    &\equidyn \bindXtoYinZ {(\bindXtoYinZ M x \ret\thunk\ret x)} w \ret \thunk (\bindXtoYinZ {\force w} x N)\tag{$\u F\eta$}\\
+    &\equidyn \bindXtoYinZ {\ret\thunk M} w \ret \thunk (\bindXtoYinZ {\force w} x N)\tag{$M$ thunkable}\\
+    &\equidyn  \ret \thunk (\bindXtoYinZ {\force \thunk M} x N)\tag{$\u F\beta$}\\
+    &\equidyn  \ret \thunk (\bindXtoYinZ {M} x N)\tag{$U\beta$}\\
   \end{align*}
 \end{proof}
 
@@ -3282,40 +3319,265 @@ variable $x$ of type $U\u B$ ``always forces $x$ when forced'':
   \vdash \simp V : \u F A$ is thunkable.
 \end{lemma}
 \begin{proof}
+  Introduction forms follow from return is thunkable and thunkables
+  compose. For elimination forms it is sufficient to show that when
+  the branches of pattern matching are thunkable, the pattern match
+  is thunkable.
   \begin{enumerate}
-    Introduction forms follow from return is thunkable and thunkables
-    compose. For elimination forms it is sufficient to show that when
-    the branches of pattern matching are thunkable, the pattern match
-    is thunkable.
-    
-  \item $\inl V$: We need to show, assuming $M$ is thunkable that
-    \[ \ret \thunk {(\bindXtoYinZ M x \ret\inl x)} \equidyn
-    \bindXtoYinZ {(\bindXtoYinZ M x \ret\inl x)} y \ret\thunk\ret y
+  \item $x$: We need to show $\simp x = \ret x$ is thunkable, which we
+    proved as a lemma above.
+  \item{} $0$ elim, we need to show 
+    \[ \bindXtoYinZ {\absurd V} y \ret\thunk\ret y\equidyn \ret\thunk {\absurd V}\]
+    but by $\eta0$ both sides are equivalent to $\absurd V$.
+  \item{} $+$ elim, we need to show
+    \[
+    \ret\thunk (\caseofXthenYelseZ V {x_1. M_1} {x_2. M_2})
+    \equidyn 
+    \bindXtoYinZ {(\caseofXthenYelseZ V {x_1. M_1} {x_2. M_2})} y \ret\thunk \ret y
     \]
     \begin{align*}
-      \bindXtoYinZ {(\bindXtoYinZ M x \ret\inl x)} y \ret\thunk\ret y\\
+      &\ret\thunk (\caseofXthenYelseZ V {x_1. M_1} {x_2. M_2})\\
       &\equidyn
-      \bindXtoYinZ M x \bindXtoYinZ {\ret\inl x} y \ret\thunk\ret y\\
-      &
+      \caseofX V \tag{$+\eta$}\\
+      &\qquad\thenY {x_1. \ret\thunk (\caseofXthenYelseZ {\inl x_1} {x_1. M_1} {x_2. M_2})}\\
+      &\qquad\elseZ {x_2. \ret\thunk (\caseofXthenYelseZ {\inr x_2} {x_1. M_1} {x_2. M_2})}\\
+      %%%%%%%%
+      &\equidyn\caseofX V \tag{$+\beta$}\\
+      &\qquad\thenY {x_1. \ret\thunk M_1}\\
+      &\qquad\elseZ {x_2. \ret\thunk M_2}\\
+      %%%%%%%%
+      &\equidyn\caseofX V \tag{$M_1,M_2$ thunkable}\\
+      &\qquad\thenY {x_1. \bindXtoYinZ {M_1} y \ret\thunk\ret y}\\
+      &\qquad\elseZ {x_2. \bindXtoYinZ {M_2} y \ret\thunk\ret y}\\
+      &\equidyn \bindXtoYinZ {(\caseofXthenYelseZ V {x_1. M_1}{x_2. M_2})} y \ret\thunk\ret y\tag{commuting conversion}\\
+    \end{align*}
+  \item{} $\times$ elim
+    \begin{align*}
+      &\ret\thunk (\pmpairWtoXYinZ V x y M)\\
+      &\equidyn \pmpairWtoXYinZ V x y \ret\thunk \pmpairWtoXYinZ {(x,y)} x y M\tag{$\times\eta$}\\
+      &\equidyn \pmpairWtoXYinZ V x y \ret\thunk M\tag{$\times\beta$}\\
+      &\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
+    \begin{align*}
+      &\ret\thunk (\pmmuXtoYinZ V x M)\\
+      &\equidyn \pmmuXtoYinZ V x \ret\thunk \pmmuXtoYinZ {\roll x} x M\tag{$\mu\eta$}\\
+      &\equidyn \pmmuXtoYinZ V x \ret\thunk M\tag{$\mu\beta$}\\
+      &\equidyn \pmmuXtoYinZ V x \bindXtoYinZ M y \ret\thunk\ret y\tag{$M$ thunkable}\\
+      &\equidyn \bindXtoYinZ {(\pmmuXtoYinZ V x M)} y \ret\thunk\ret y\tag{commuting conversion}
     \end{align*}
-    
   \end{enumerate}
 \end{proof}
+
+Dually, we have that a stack out of a force is linear and that linears
+are closed under composition, so we can easily build up bigger linear
+morphisms from smaller ones.
+\begin{lemma}[Force to a stack is Linear]
+  If $\Gamma \pipe \bullet : \u B \vdash S : \u C$, then
+  $\Gamma , x : U\u B\vdash S[\force x] : \u B$ is linear in $x$.
+\end{lemma}
+\begin{proof}
+  \begin{align*}
+    S[\force \thunk {(\bindXtoYinZ {\force z} x \force x)}]
+    &\equidyn
+    S[{(\bindXtoYinZ {\force z} x \force x)}]\tag{$U\beta$}\\
+    &\equidyn \bindXtoYinZ {\force z} x S[\force x] \tag{$\u F\eta$}
+  \end{align*}
+\end{proof}
+
+\begin{lemma}[Linear Terms Compose]
+  If $\Gamma , x : U \u B \vdash M : \u B'$ is linear in $x$ and
+  $\Gamma , y : \u B' \vdash N : \u B''$ is linear in $y$, then
+  $\Gamma , x : U \u B \vdash N[\thunk M/y] : $
+\end{lemma}
+\begin{proof}
+  \begin{align*}
+    &N[\thunk M/y][\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]\\
+    &= N[\thunk {(M[\thunk{(\bindXtoYinZ {\force z} x \force x)}])}/y]\\
+    &\equidyn N[\thunk {(\bindXtoYinZ {\force z} x M)}/y]\tag{$M$ linear}\\
+    &\equidyn N[\thunk{(\bindXtoYinZ {\force z} x \force \thunk M)}/y] \tag{$U\beta$}\\
+    &\equidyn
+    N[\thunk{(\bindXtoYinZ {\force z} x \bindXtoYinZ {\ret\thunk M} y \force y)}/y] \tag{$\u F\beta$}\\
+    &\equidyn
+    N[\thunk{(\bindXtoYinZ {(\bindXtoYinZ {\force z} x \ret\thunk M)} y \force y)}/y] \tag{$\u F\eta$}\\
+    &\equidyn
+    N[\thunk{(\bindXtoYinZ {\force w} y \force y)}/y][\thunk(\bindXtoYinZ {\force z} x \ret\thunk M)/w] \tag{$U\beta$}\\
+    &\equidyn (\bindXtoYinZ {\force w} y N)[\thunk (\bindXtoYinZ {\force z} x \ret \thunk M)/w] \tag{$N$ linear}\\
+    &\equidyn (\bindXtoYinZ {(\bindXtoYinZ {\force z} x \ret \thunk M)} y N) \tag{$U\beta$}\\
+    &\equidyn (\bindXtoYinZ {\force z} x \bindXtoYinZ {\ret\thunk M} y N \tag{$\u F\eta$}\\
+    &\equidyn \bindXtoYinZ {\force z} x N[\thunk M/y]
+  \end{align*}
+\end{proof}
+
 \begin{lemma}[Complex Stacks Simplify to Linear Terms]
   If $\Gamma\pipe \bullet : \u B \vdash S : \u C$ is a (possibly)
   complex stack, then $\Gamma, z : U\u B \vdash \simpp{S[\force z]} :
   \u C$ is linear in $z$.
 \end{lemma}
 \begin{proof}
-  TODO
+  There are $4$ classes of rules for complex stacks: those that are
+  rules for simple stacks ($\bullet$, computation type elimination
+  forms), introduction rules for negative computation types where the
+  subterms are complex stacks, elimination of positive value types
+  where the continuations are complex stacks and finally application
+  to a complex value.
+
+  The rules for simple stacks are easy: they follow immediately from
+  the fact that forcing to a stack is linear and that complex stacks
+  compose.  For the negative introduction forms, we have to show that
+  binding commutes with introduction forms. For pattern matching
+  forms, we just need commuting conversions. For function application,
+  we use the lemma that binding a thunkable in a linear term is
+  linear.
+  \begin{enumerate}
+  \item $\bullet$: This is just saying that $\force x$ is linear, which we showed above.
+  \item $\to$ elim We need to show, assuming that $\Gamma, x : \u B
+    \vdash M : \u C$ is linear in $x$ and $\Gamma \vdash N : \u F A$
+    is thunkable, that
+    \[
+    \bindXtoYinZ N y M\,y
+    \]
+    is linear in $x$.
+    \begin{align*}
+      &\bindXtoYinZ N y (M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x])\,y\\
+      &\equidyn \bindXtoYinZ N y (\bindXtoYinZ {\force z} x M)\,y \tag{$M$ linear in $x$}\\
+      &\equidyn \bindXtoYinZ N y \bindXtoYinZ {\force z} x M\,y \tag{$\u F\eta$}\\
+      &\equidyn \bindXtoYinZ {\force z} x \bindXtoYinZ N y M\,y\tag{thunkables are central}
+    \end{align*}
+  \item $\to$ intro
+    \begin{align*}
+      & \lambda y:A. M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]\\
+      &\equidyn \lambda y:A. \bindXtoYinZ {\force z} x M \tag{$M$ is linear}\\
+      &\equidyn \lambda y:A. \bindXtoYinZ {\force z} x (\lambda y:A. M)\, y \tag{$\to\beta$}\\
+      &\equidyn \lambda y:A. (\bindXtoYinZ {\force z} x (\lambda y:A. M))\, y \tag{$\u F\eta$}\\
+      &\equidyn \bindXtoYinZ {\force z} x (\lambda y:A. M) \tag{$\to\eta$}
+    \end{align*}
+  \item $\top$ intro
+    We need to show
+    \[ \bindXtoYinZ {\force z} w \{\} \equidyn \{\} \]
+    Which is immediate by $\top\eta$
+  \item $\with$ intro
+    \begin{align*}
+      &     \pairone{M[\thunk {(\bindXtoYinZ {\force z} x \force x)}]/x}\\
+      &\pairtwo{N[\thunk {(\bindXtoYinZ {\force z} x \force x)}/x]}\\
+      &\equidyn \pairone{\bindXtoYinZ {\force z} x M}\tag{$M, N$ linear}\\
+      &\qquad    \pairtwo{\bindXtoYinZ {\force z} x N}\\
+      &\equidyn \pairone{\bindXtoYinZ {\force z} x {\pi \pair M N}}\tag{$\with\beta$}\\
+      &\qquad    \pairtwo{\bindXtoYinZ {\force z} x {\pi' \pair M N}}\\
+      &\equidyn \pairone{\pi({\bindXtoYinZ {\force z} x \pair M N})}\tag{$\u F\eta$}\\
+      &\qquad    \pairtwo{\pi'({\bindXtoYinZ {\force z} x \pair M N})}\\
+      &\equidyn \bindXtoYinZ {\force z} x \pair M N\tag{$\with\eta$}
+    \end{align*}
+  \item $\nu$ intro
+    \begin{align*}
+      & \roll M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]\\
+      &\equidyn \roll (\bindXtoYinZ {\force z} x M) \tag{$M$ is linear} \\
+      &\equidyn \roll (\bindXtoYinZ {\force z} x \unroll \roll M) \tag{$\nu\beta$}\\
+      &\equidyn \roll \unroll (\bindXtoYinZ {\force z} x \roll M) \tag{$\u F\eta$}\\
+      &\equidyn \bindXtoYinZ {\force z} x (\roll M) \tag{$\nu\eta$}
+    \end{align*}
+  \item $\u F$ elim: Assume $\Gamma, x : A \vdash M : \u F A'$ and
+    $\Gamma, y : A' \vdash N : \u B$, then we need to show
+    \[ \bindXtoYinZ M y N \]
+    is linear in $M$.
+    \begin{align*}
+      & \bindXtoYinZ {M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]} y N\\
+      & \equidyn
+      \bindXtoYinZ {(\bindXtoYinZ {\force z} x M)} y N\tag{$M$ is linear}\\
+      &\equidyn
+      \bindXtoYinZ {\force z} x \bindXtoYinZ M y N\tag{$\u F\eta$}
+    \end{align*}
+    % Value elimination forms 0, +, 1, x,
+  \item $0$ elim: We want to show $\Gamma, x:U\u B \vdash \absurd V :
+    \u C$ is linear in $x$, which means showing:
+    \[ \absurd V \equidyn \bindXtoYinZ {\force z} x \absurd V
+    \]
+    which follows from $0\eta$
+  \item $+$ elim: Assuming $\Gamma, x : U\u B, y_1 : A_1 \vdash M_1 :
+    \u C$ and $\Gamma, x : U\u B, y_2: A_2\vdash M_2 : \u C$ are
+    linear in $x$, and $\Gamma \vdash V : A_1 + A_2$, we need to show
+    \[ \caseofXthenYelseZ V {y_1. M_1} {y_2. M_2} \]
+    is linear in $x$.
+    \begin{align*}
+      & \caseofXthenYelseZ V {y_1. M_1[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]} {y_2. M_2[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]}\\
+      &\equidyn \caseofXthenYelseZ V {y_1. \bindXtoYinZ {\force z} x M_1}{y_2. \bindXtoYinZ {\force z} x M_2}\tag{$M_1,M_2$ linear}\\
+      &\equidyn
+       \bindXtoYinZ {\force z} x \caseofXthenYelseZ V {y_1. M_1}{y_2. M_2}
+    \end{align*}
+  \item $\times$ elim: Assuming $\Gamma, x:U\u B, y_1 : A_1, y_2 : A_2
+    \vdash M : \u B$ is linear in $x$ and $\Gamma \vdash V : A_1
+    \times A_2$, we need to show
+    \[ \pmpairWtoXYinZ V {y_1}{y_2} M \]
+    is linear in $x$.
+    \begin{align*}
+      &\pmpairWtoXYinZ V {y_1}{y_2} M[[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]]\\
+      &\equidyn \pmpairWtoXYinZ V {y_1}{y_2} \bindXtoYinZ {\force z} x M\tag{$M$ linear}\\
+      &\equidyn  \bindXtoYinZ {\force z} x\pmpairWtoXYinZ V {y_1}{y_2} M\tag{comm. conv}\\
+    \end{align*}
+  \item $\mu$ elim: Assuming $\Gamma , x : U \u B, y : A[\mu X.A/X]
+    \vdash M : \u C$ is linear in $x$ and $\Gamma \vdash V : \mu X.A$,
+    we need to show
+    \[ \pmmuXtoYinZ V y M \]
+    is linear in $x$.
+    \begin{align*}
+      & \pmmuXtoYinZ V y M[\thunk{(\bindXtoYinZ {\force z} x \force x)}/x]\\
+      & \equidyn \pmmuXtoYinZ V y \bindXtoYinZ {\force z} x M\tag{$M$ linear}\\
+      &\equidyn  \bindXtoYinZ {\force z} x\pmmuXtoYinZ V y M \tag{commuting conversion}
+    \end{align*}
+  \end{enumerate}
 \end{proof}
 
+\begin{lemma}[Compositionality of De-complexification]
+  \begin{enumerate}
+  \item If $\Gamma, x : A\vdash M : \u B$ and $\Gamma \vdash V : A$
+    are complex terms, then
+    \[ 
+    \simpp{M[V/x]} \equidyn \bindXtoYinZ {\simp V} x {\simp M}
+    \]
+  %% \item If $\Gamma, x : A\pipe \bullet : \u C \vdash S : \u B$ and $\Gamma \vdash V : A$
+  %%   are complex terms, then
+  %%   \[ 
+  %%   \simpp{S[V/x][\force z]} \equidyn \bindXtoYinZ {\simp V} x {\simp {S[\force z]}}
+  %%   \]
+    
+  %% TODO: other cases
+  %% \item If $\Gamma\pipe \bullet : \u B\vdash S : \u C$ and $\Gamma \vdash M : \u B$, then
+  %%   \[
+  %%   \simpp{S[M]} \equidyn \simpp{S[\force x]}[\simp ]
+    %% \]
+  \end{enumerate}
+\end{lemma}
+
 % Which parts are hard? substitution rule I think
 \begin{theorem}[De-complexification preserves Dynamism]
+  
   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]
@@ -3350,35 +3612,6 @@ variable $x$ of type $U\u B$ ``always forces $x$ when forced'':
   \[ M \equidyn \simp M \ltdyn \simp {M'} \equidyn M' \]
 \end{proof}
 
-This translates any term with complex values in it to an equivalent
-(i.e. $\equidyn$) one without complex values, showing that while
-complex values are convenient for reasoning, they are not ultimately
-\emph{necessary} for compuatation.
-%
-The high-level idea behind the translation is that complex values all
-consist of pattern matching where the continuation is a value, such as
-$\pmpairWtoXYinZ V x y V'$.
-%
-Since our notion of a whole program is a term, and not a value, this
-pattern match appears in the context of a larger term: either in a
-return, or a function application.
-%
-Since pattern matching is always a safe operation, it can be lifted up
-to the term level, so for instance:
-\[ \ret \pmpairWtoXYinZ V x y V' \equidyn \pmpairWtoXYinZ V x y \ret V'\]
-and
-\[ M\, \pmpairWtoXYinZ V x y V' \equidyn \pmpairWtoXYinZ V x y M\, V'\]
-In the equational theory, this transformation is justified by the
-$\eta$ laws for the value types: they say exactly that pattern matches
-are safe to perform at any point.
-%
-Note that this can lead to a large blowup of term size, when
-eliminating pattern matching for sums.
-
-Our pass is almost exactly the same as the one given in the CBPV
-monograph (TODO cite), and so we relegate the details to the extended
-version/appendix.
-
 \subsection{Call-by-push-value Inequational Theory}
 
 Next, we give the inequational theory for our CBPV language.
@@ -3648,6 +3881,18 @@ Next, we give the inequational theory for our CBPV language.
   \caption{Call-by-push-value logical and error rules}
 \end{figure}
 
+\section{Operational Graduality}
+
+In this section we establish a model of our CBPV inequational theory
+using a notion of observational approximation based on the CBPV
+operational semantics.
+%
+By composition with the axiomatic graduality theorem, this establishes
+the \emph{operational graduality} theorem, i.e., a theorem analogous
+to the \emph{dynamic gradual guarantee} as presented in TODO cite.
+
+TODO: show the ``goal theorem''
+
 \subsection{Call-by-push-value operational semantics}
 
 We present the operational semantics for our CBPV in figure TODO ref.