diff --git a/paper.tex b/paper.tex
index 07fbde1..de52df9 100644
--- a/paper.tex
+++ b/paper.tex
@@ -1441,7 +1441,7 @@ \subsection{Expressions}
   separate rule since, while it follows trivially from $\beta$ for pure $a$, we also want to
   consider \emph{impure} expressions with some effect $e \neq \bot$.
   
-  \item Rules \brle{let$_1$-op}, \brle{let$_1$-inl}, and \brle{let$_1$-inr},
+  \item Rules \brle{let$_1$-op}, \brle{let$_1$-let$_1$}, \brle{let$_1$-let$_2$},
   \brle{let$_1$-abort}, and \brle{let$_1$-case} which allow us to ``pull'' a let-statement out of
   any of the other expression constructors; operationally, this is saying that the bound expression
   we pull out is evaluated before the rest of the \ms{let}-binding.
@@ -1502,18 +1502,18 @@ \subsection{Expressions}
         {\letexpr{z}{(\letexpr{(x, y)}{e}{c})}{d}}
         {\letexpr{(x, y)}{e}{\letexpr{z}{c}{d}}}{D}}
     \\
-    \prftree[r]{\rle{let$_1$-inl}}
-      {\hasty{\Gamma}{\epsilon}{a}{A}}
-      {\hasty{\Gamma, \bhyp{x}{A + B}}{\epsilon}{c}{C}}
-      {\hasty{\Gamma, \bhyp{y}{C}}{\epsilon}{d}{D}}
-      {\tmeq{\Gamma}{\epsilon}{\letexpr{y}{\linl{a}}{c}}{\letexpr{x}{a}{\letexpr{y}{\linl{x}}{c}}}{C}}
-    \\
-    \prftree[r]{\rle{let$_1$-inr}}
-      {\hasty{\Gamma}{\epsilon}{b}{B}}
-      {\hasty{\Gamma, \bhyp{x}{A + B}}{\epsilon}{c}{C}}
-      {\hasty{\Gamma, \bhyp{y}{C}}{\epsilon}{d}{D}}
-      {\tmeq{\Gamma}{\epsilon}{\letexpr{y}{\linr{b}}{c}}{\letexpr{x}{b}{\letexpr{y}{\linr{x}}{c}}}{C}}
-    \\
+    % \prftree[r]{\rle{let$_1$-inl}}
+    %   {\hasty{\Gamma}{\epsilon}{a}{A}}
+    %   {\hasty{\Gamma, \bhyp{x}{A + B}}{\epsilon}{c}{C}}
+    %   {\hasty{\Gamma, \bhyp{y}{C}}{\epsilon}{d}{D}}
+    %   {\tmeq{\Gamma}{\epsilon}{\letexpr{y}{\linl{a}}{c}}{\letexpr{x}{a}{\letexpr{y}{\linl{x}}{c}}}{C}}
+    % \\
+    % \prftree[r]{\rle{let$_1$-inr}}
+    %   {\hasty{\Gamma}{\epsilon}{b}{B}}
+    %   {\hasty{\Gamma, \bhyp{x}{A + B}}{\epsilon}{c}{C}}
+    %   {\hasty{\Gamma, \bhyp{y}{C}}{\epsilon}{d}{D}}
+    %   {\tmeq{\Gamma}{\epsilon}{\letexpr{y}{\linr{b}}{c}}{\letexpr{x}{b}{\letexpr{y}{\linr{x}}{c}}}{C}}
+    % \\
     \prftree[r]{\rle{let$_1$-abort}}
       {\hasty{\Gamma}{\epsilon}{a}{\mb{0}}}
       {\hasty{\Gamma, \bhyp{y}{A}}{\epsilon}{b}{B}}
@@ -1675,10 +1675,9 @@ \subsection{Regions}
 \begin{itemize}
   \item \brle{let$_1$-$\beta$} allows us to perform $\beta$-reduction of \emph{pure} expressions
   into regions; unlike for terms, we do not need an $\eta$-rule
-  \item Exactly like for \ms{let}-expressions, \brle{let$_1$-op},
-  \brle{let$_1$-inl}, \brle{let$_1$-inr}, \brle{let$_1$-abort}, and \brle{let$_1$-case} allow us
-  to pull out nested subexpressions of the bound value of a \ms{let}-statement into their own
-  unary \ms{let}-statement
+  \item Exactly like for \ms{let}-expressions, \brle{let$_1$-op}, \brle{let$_1$-let$_1$},
+  \brle{let$_1$-let$_2$}, \brle{let$_1$-abort}, and \brle{let$_1$-case} allow us to pull out nested
+  subexpressions of the bound value of a \ms{let}-statement into their own unary \ms{let}-statement
 \end{itemize}
 Similarly to expressions, binary \ms{let}-statements and \ms{case}-statements need only the obvious
 $\beta$ rule and binding rule, with all the interactions with other constructors derivable; these
@@ -1765,16 +1764,16 @@ \subsection{Regions}
         {\letstmt{(x, y)}{e}{\letstmt{z}{c}{r}}}
         {\ms{L}}}
     \\
-    \prftree[r]{\rle{let$_1$-inl}}
-      {\hasty{\Gamma}{\epsilon}{a}{A}}
-      {\haslb{\Gamma, \bhyp{y}{A + B}}{r}{\ms{L}}}
-      {\lbeq{\Gamma}{\letstmt{y}{\linl{a}}{r}}{\letstmt{x}{a}{\letstmt{y}{\linl{x}}{r}}}{\ms{L}}}
-    \\
-    \prftree[r]{\rle{let$_1$-inr}}
-      {\hasty{\Gamma}{\epsilon}{b}{B}}
-      {\haslb{\Gamma, \bhyp{y}{A + B}}{r}{\ms{L}}}
-      {\lbeq{\Gamma}{\letstmt{y}{\linr{b}}{r}}{\letstmt{x}{b}{\letstmt{y}{\linr{x}}{r}}}{\ms{L}}}
-    \\
+    % \prftree[r]{\rle{let$_1$-inl}}
+    %   {\hasty{\Gamma}{\epsilon}{a}{A}}
+    %   {\haslb{\Gamma, \bhyp{y}{A + B}}{r}{\ms{L}}}
+    %   {\lbeq{\Gamma}{\letstmt{y}{\linl{a}}{r}}{\letstmt{x}{a}{\letstmt{y}{\linl{x}}{r}}}{\ms{L}}}
+    % \\
+    % \prftree[r]{\rle{let$_1$-inr}}
+    %   {\hasty{\Gamma}{\epsilon}{b}{B}}
+    %   {\haslb{\Gamma, \bhyp{y}{A + B}}{r}{\ms{L}}}
+    %   {\lbeq{\Gamma}{\letstmt{y}{\linr{b}}{r}}{\letstmt{x}{b}{\letstmt{y}{\linr{x}}{r}}}{\ms{L}}}
+    % \\
     \\
     \prftree[r]{\rle{let$_1$-case}}
       {\hasty{\Gamma}{\epsilon}{e}{A + B}}
@@ -7858,8 +7857,7 @@ \subsection{Equational Theory}
         ; \dnt{\hasty{\Gamma, \bhyp{y}{B}}{\epsilon}{c}{C}} \\
       & = \dnt{\hasty{\Gamma}{\epsilon}{\letexpr{y}{f\;a}{c}}{C}}
     \end{align*}
-    as desired. The cases \brle{let$_1$-inl}, \brle{let$_1$-inr}, and \brle{let$_1$-abort} are
-    analogous.
+    as desired. The \brle{let$_1$-abort} case is analogous.
     \item \brle{let$_1$-let$_1$}: we have that
     \begin{align*}
       & \dnt{\hasty{\Gamma}{\epsilon}{\letexpr{y}{(\letexpr{x}{a}{b}}{c})}{C}} \\