diff --git a/paper/gtt.tex b/paper/gtt.tex
index c6065fad08d815bffa1d0b9aba01cc27445a9b4e..d9a0932841a200e921757e7997f3349c3f5101f7 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -2430,8 +2430,9 @@ embeddings but I don't see anywhere where we need that.
   \end{mathpar}
 \end{proof}
 
-TODO: we don't ``need'' this lemma, except to show that GTT is an
-``extension'' of the homogeneous ordering
+The following lemma is key to proving many ``axioms'' are valid in
+GTT, since an identity cast is inserted in translation. Also it is key
+to proving that GTT is a conservative extension of CBPV.
 \begin{lemma}[Identity Expansion]
   For any $A$ and $\u B$,
   \begin{mathpar}
@@ -2551,24 +2552,220 @@ TODO: we don't ``need'' this lemma, except to show that GTT is an
   For compatibility rules a pattern emerges.  For universal rules
   (positive intro, negative elim) are easy, don't need to reason about
   casts at all. For ``(co)-pattern matching rules'' (positive elim,
-  negative intro), a cast needs to be introduced at a redex and we
-  need to use the \emph{projection} property of casts.  Fortunately,
-  all reasoning about ``shifted'' casts is handled in lemmas, here we
-  only deal with ``nice'' casts.
+  negative intro), we need to invoke the $\eta$ principle (or
+  commuting conversion, which is derived from the $\eta$ principle).
+  In all compatibility cases, the cast reductions lemma keeps the
+  proof straightforward.
+
+  Fortunately, all reasoning about ``shifted'' casts is handled in
+  lemmas, here we only deal with ``nice'' casts.
   \begin{enumerate}
     %%  Logical rules:
-  \item TODO: Transitivity
-  \item TODO: Substitution
-  \item TODO: Variables
-  \item TODO: Hole
-    %% Error Rules
-  \item TODO: error is bottom
-  \item TODO: error strictness
-    %% Cast Rules
-  \item TODO: UpCast-L
-  \item TODO: UpCast-R
-  \item TODO: DnCast-R
-  \item TODO: DnCast-L
+  \item Transitivity for values: The GTT rule is
+    \[
+    \inferrule{
+    \Phi : \Gamma \ltdyn \Gamma' \and \Phi' : \Gamma' \ltdyn \Gamma'' \and
+    \Phi'' : \Gamma \ltdyn \Gamma''
+    \\
+    \Phi \vdash V \ltdyn V' : A \ltdyn A'\\
+    \Phi' \vdash V' \ltdyn V'' : A' \ltdyn A''\\
+    }
+    { \Phi'' \vdash V \ltdyn V'' : A \ltdyn A''}
+    \]
+    Which under translation (and the same assumptions about the contexts) is
+    \[
+    \inferrule
+    {\sem{\Gamma} \vdash \supcast{A}{A'}[\sem{V}] \ltdyn \sem{V'}[\sem{\Phi}] : \sem{A'}\\
+     \sem{\Gamma'} \vdash \supcast{A'}{A'}[\sem{V'}] \ltdyn \sem{V''}[\sem{\Phi'}] : \sem{A''}
+    }
+    {\sem{\Gamma} \vdash \supcast{A}{A''}[\sem{V}] \ltdyn \sem{V''}[\sem{\Phi''}] : \sem{A''}}
+    \]
+    We proceed as follows, the key lemma here is the cast decomposition lemma:
+    \begin{align*}
+      \supcast{A}{A''}[\sem{V}]
+      &\equidyn
+      \supcast{A'}{A''}[\supcast{A}{A'}[\sem{V}]] \tag{cast decomposition}\\
+      &\ltdyn \supcast{A'}{A''}[\sem{V'}[\sem{\Phi}]] \tag{IH}\\
+      &\ltdyn \sem{V''}[\sem{\Phi'}][\sem{\Phi}] \tag{IH}\\
+      &\equidyn \sem{V''}[\sem{\Phi''}] \tag{cast decomposition}
+    \end{align*}
+  \item Transitivity for terms:
+    The GTT rule is
+    \[
+    \inferrule{
+    \Phi : \Gamma \ltdyn \Gamma' \and \Phi' : \Gamma' \ltdyn \Gamma'' \and
+    \Phi'' : \Gamma \ltdyn \Gamma''
+    \and \Psi : \Delta \ltdyn \Delta' \and \Psi : \Delta' \ltdyn \Delta''
+    \and \Psi'' : \Delta\ltdyn \Delta''
+    \\
+    \Phi \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'\\
+    \Phi' \pipe \Psi' \vdash M' \ltdyn M'' : \u B' \ltdyn \u B''\\
+    }
+    { \Phi'' \pipe \Psi'' \vdash M \ltdyn M'' : \u B \ltdyn \u B''}
+    \]
+    Which under translation (and the same assumptions about the contexts) is
+    \[
+    \inferrule
+    {\sem{\Gamma} \pipe \sem{\Delta'} \vdash \sem{M}[\sem{\Psi}] \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Phi}]] : \sem{\u B}\\
+    \sem{\Gamma'} \pipe \sem{\Delta''} \vdash \sem{M'}[\sem{\Psi'}] \ltdyn \sdncast{\u B'}{\u B''}[\sem{M''}[\sem{\Phi'}]] : \sem{\u B'}}
+    {\sem{\Gamma} \pipe \sem{\Delta''} \vdash \sem{M}[\sem{\Psi''}] \ltdyn \sdncast{\u B}{\u B''}[\sem{M''}[\sem{\Phi''}]] : \sem{\u B}}
+    \]
+    We proceed as follows, the key lemma here is the cast decomposition lemma:
+    \begin{align*}
+      \sem{M}[\sem{\Psi''}]
+      &\equidyn
+      \sem{M}[\sem{\Psi}][\sem{\Psi'}] \tag{Cast decomposition}\\
+      &\ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem{\Psi'}][\sem{\Phi}]]\tag{IH}\\
+      &\ltdyn \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B''}[\sem{M''}[\sem{\Phi'}][\sem{\Phi}]]]\tag{IH}\\
+      &\equidyn \sdncast{\u B}{\u B''}[\sem{M''}[\sem{\Phi''}]] \tag{Cast decomposition}
+    \end{align*}
+  \item Substitution of a value in a value:
+    The GTT rule is
+    \[
+    \inferrule
+    {\Phi, x \ltdyn x' : A_1 \ltdyn A_1' \vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'\\
+    \Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'}
+    {\Phi \vdash V_2[V_1/x]\ltdyn V_2'[V_1'/x'] : A_2 \ltdyn A_2'}
+    \]
+    Where $\Phi : \Gamma \ltdyn \Gamma'$. Under translation, we need to show
+    \[
+    \inferrule
+    {\sem\Gamma, x : \sem{A_1} \vdash \supcast{A_2}{A_2'}[\sem{V_2}] \ltdyn \sem{V_2'}[\sem\Phi][\supcast{A_1}{A_1'}[x]/x'] : \sem{A_2'}\\
+     \sem\Gamma \vdash \supcast{A_1}{A_1'}[\sem{V_1}] \ltdyn \sem{V_1'}[\sem\Phi] : \sem{A_1'}}
+    {\sem\Gamma \vdash \supcast{A_2}{A_2'}[\sem{V_2[V_1/x]}] \ltdyn \sem{V_2'[V_1'/x']}[\sem\Phi] : \sem{A_2'}}
+    \]
+    Which follows by compositionality:
+    \begin{align*}
+      \supcast{A_2}{A_2'}[\sem{V_2[V_1/x]}]
+      &= (\supcast{A_2}{A_2'}[\sem{V_2}])[\sem{V_1}/x] \tag{Compositionality}\\
+      &\ltdyn \sem{V_2'}[\sem\Phi][\supcast{A_1}{A_1'}[x]/x'][\sem{V_1}/x]\tag{IH}\\
+      &= \sem{V_2'}[\sem\Phi][\supcast{A_1}{A_1'}[\sem{V_1}]/x']\\
+      &\ltdyn \sem{V_2'}[\sem\Phi][\sem{V_1'}[\sem\Phi]/x']\tag{IH}\\
+      &= \sem{V_2'[V_1'/x']}[\sem\Phi]
+    \end{align*}
+  \item Substitution of a value in a term:
+    The GTT rule is
+    \[
+    \inferrule
+    {\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'\\
+      \Phi \vdash V \ltdyn V' : A \ltdyn A'
+    }
+    {\Phi \vdash M[V/x] \ltdyn M'[V'/x'] : \u B \ltdyn \u B'}
+    \]
+    Where $\Phi : \Gamma \ltdyn \Gamma'$ and $\Psi : \Delta \ltdyn \Delta'$.
+    Under translation this is:
+    \[
+    \inferrule
+    {\sem\Gamma, x : \sem{A} \pipe \sem\Delta \vdash \sem M \ltdyn \sdncast{\u B}{\u B'}[\sem {M'}[\sem\Phi][\supcast{A}{A'}[x]/x']] : \sem{\u B}\\
+    \sem\Gamma \vdash \supcast{A}{A'}[{\sem V}] \ltdyn \sem{V'}[\sem\Phi] : \sem{A'}}
+    {\sem\Gamma \pipe \sem\Delta \vdash \sem {M[V/x]} \ltdyn \sdncast{\u B}{\u B'}[\sem{M'[V'/x']}[\sem\Phi]] : \sem{\u B}}
+    \]
+    Which follows from compositionality of the translation:
+    \begin{align*}
+      \sem {M[V/x]}
+      &= \sem{M}[\sem{V}/x] \tag{Compositionality}\\
+      &\ltdyn \sdncast{\u B}{\u B'}[\sem {M'}[\sem\Phi][\supcast{A}{A'}[x]/x']][\sem{V}/x] \tag{IH}\\
+      &= \sdncast{\u B}{\u B'}[\sem {M'}[\sem\Phi][\supcast{A}{A'}[\sem{V}]/x']]\\
+      &\ltdyn \sdncast{\u B}{\u B'}[\sem {M'}[\sem\Phi][\sem{V'}[\sem\Phi]/x']]\tag{IH}\\
+      &= \sdncast{\u B}{\u B'}[\sem{M'[V'/x']}[\sem\Phi]] \tag{Compositionality}
+    \end{align*}
+  \item Substitution of a term in a stack:
+    The GTT rule is
+    \[
+    \inferrule
+    {\Phi \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash S \ltdyn S' : \u C \ltdyn \u C'\\
+      \Phi \pipe \cdot \vdash M \ltdyn M' : \u B \ltdyn \u B'}
+    {\Phi \pipe \cdot \vdash S[M]\ltdyn S'[M'] : \u C \ltdyn \u C'}
+    \]
+    Where $\Phi : \Gamma \ltdyn \Gamma'$.
+    Under translation this is
+    \[
+    \inferrule
+    {\sem\Gamma \pipe \bullet : \sem{\u B'} \vdash \sem{S}[\sdncast{\u B}{\u B'}[\bullet]] \ltdyn \sdncast{\u C}{\u C'}[\sem{S'}[\sem\Phi]] : \sem{\u C}\\
+      \sem\Gamma \pipe \cdot \vdash \sem{M} \ltdyn \sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]] : \sem{\u B}}
+    {\sem\Gamma \pipe \cdot \vdash \sem{S[M]} \ltdyn \sdncast{\u C}{\u C'}[\sem{S'[M']}[\sem\Phi]] : \sem{\u C}}
+    \]
+    We follows easily using compositionality of the translation:
+    \begin{align*}
+      \sem{S[M]}
+      &= \sem{S}[\sem{M}] \tag{Compositionality}\\
+      &\ltdyn   \sem{S}[\sdncast{\u B}{\u B'}[\sem{M'}[\sem\Phi]]] \tag{IH}\\
+      &\ltdyn   \sdncast{\u C}{\u C'}[\sem{S'}[\sem\Phi][\sem{M'}[\sem\Phi]]]\tag{IH}\\
+      &= \sdncast{\u C}{\u C'}[\sem{S'[M']}[\sem\Phi]] \tag{Compositionality}
+    \end{align*}
+  \item Variables: The GTT rule is
+    \[ \Gamma_1 \ltdyn \Gamma_1' ,x \ltdyn x' : A \ltdyn A', \Gamma_2 \ltdyn \Gamma_2' \vdash x \ltdyn x' : A \ltdyn A' \]
+    which under translation is
+    \[ \sem{\Gamma_1}, x : \sem A, \sem{\Gamma_2} \vdash \supcast{A}{A'}[x] \ltdyn \supcast{A}{A'}[x] : \sem{A'} \]
+    which is an instance of reflexivity.
+  \item Hole: The GTT rule is
+    \[ \Phi \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \bullet : \u B \ltdyn \u B' \]
+    which under translation is
+    \[ \sem\Gamma \pipe \bullet : \u B' \vdash \sdncast{\u B}{\u B'}[\bullet] \ltdyn \sdncast{\u B}{\u B'}[\bullet] : \u B \]
+    which is an instance of reflexivity.
+    %% Error Axioms
+  \item Error is bottom: The GTT axiom is
+    \[ \Phi \vdash \err \ltdyn M : \u B \]
+    where $\Phi : \Gamma \ltdyn \Gamma'$, so we need to show
+    \[ \sem\Gamma \vdash \err \ltdyn \sdncast{\u B}{\u B}[\sem{M}[\sem{\Phi}]] : \sem{\u B} \]
+    which is an instance of the error is bottom axiom of CBPV.
+  \item Error strictness: The GTT axiom is
+    \[
+    \Phi \vdash S[\err] \ltdyn \err : \u B
+    \]
+    where $\Phi : \Gamma \ltdyn \Gamma'$, which under translation is
+    \[
+    \sem\Gamma \vdash \sem{S}[\err] \ltdyn \sdncast{\u B}{\u B}[\err] : \sem{\u B}
+    \]
+    By strictness of stacks in CBPV, both sides are equivalent to
+    $\err$, so it follows by reflexivity.
+
+    %% Cast Axioms
+  \item UpCast-L: The GTT axiom is
+    \[
+    x \ltdyn x' : A \ltdyn A' \vdash \upcast{A}{A'}x \ltdyn x' : A'
+    \]
+    which under translation is
+    \[
+    x : \sem{A} \vdash \supcast{A'}{A'}[\supcast{A}{A'}[x]] \ltdyn \supcast{A}{A'}[x] : A'
+    \]
+    Which follows by identity expansion and reflexivity.
+  \item UpCast-R: The GTT axiom is
+    \[
+    x : A \vdash x \ltdyn \upcast{A}{A'}x : A \ltdyn A'
+    \]
+    which under translation is
+    \[
+    x : \sem{A} \vdash \supcast{A}{A'}[x] \ltdyn \supcast{A}{A'}[\supcast{A}{A}[x]] : \sem{A'}
+    \]
+    which follows by identity expansion and reflexivity.
+  \item DnCast-R: The GTT axiom is
+    \[
+    \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \dncast{\u B}{\u B'} : \u B
+    \]
+    Which under translation is
+    \[
+    \bullet : \sem{\u B'} \vdash
+    \sdncast{\u B}{\u B'}[\bullet]
+    \ltdyn
+    \sdncast{\u B}{\u B}[\sdncast{\u B}{\u B'}[\bullet]]
+    : \sem{\u B}
+    \]
+    Which follows by identity expansion and reflexivity.
+  \item DnCast-L: The GTT axiom is
+    \[
+    \bullet : \u B' \vdash \dncast{\u B}{\u B'} \bullet \ltdyn \bullet : \u B \ltdyn \u B'
+    \]
+    So under translation we need to show
+    \[
+    \bullet : \sem{\u B'} \vdash
+    \sdncast{\u B}{\u B'}[\sdncast{\u B'}{\u B'}[\bullet]]
+    \ltdyn
+    \sdncast{\u B}{\u B'}\bullet : \sem{\u B}
+    \]
+    Which follows immediately by reflexivity and the lemma that
+    identity casts are identities.
+
     %% Value Compat Rules
   \item TODO: $0$ elim, we do the term case, the value case is similar
     \[