diff --git a/cbpv.mng b/cbpv.mng
index 0467411..f19dece 100644
--- a/cbpv.mng
+++ b/cbpv.mng
@@ -173,7 +173,7 @@ Because we're dealing with CBPV, values have no $\beta$ reductions,
 so there's no need for head reduction of values as there are no heads.
 Furthermore, there is only one strongly neutral value,
 so we inline the definition as a variable where needed,
-but also write it as $[[v ∈ SNe]]$ for symmetry as appropriate.
+but also write it as \fbox{$[[v ∈ SNe]]$} for symmetry as appropriate.
 Otherwise, the remaining four judgements are defined mutually below.
 
 \drules[SNe]{$[[m ∈ SNe]]$}{strongly neutral computations}{Force,App,Let,Case}
@@ -288,7 +288,7 @@ but the alternate choices likely work as well.
     or right injections whose values are in that of $[[A2]]$.
   \item Computations in the interpretation of the $[[F A]]$ type
     reduce to either a neutral computation
-    or a return whose value is in the interpretation of $[[A]]$.
+    or a returned value in the interpretation of $[[A]]$.
   \item Computations are in the interpretation of the function type $[[A → B]]$
     if applying them to values in the interpretation of $[[A]]$
     yields computations in the interpretation of $[[B]]$.
@@ -301,7 +301,7 @@ Unfortunately, this is not well defined,
 since the logical relation appears in a negative position
 (to the left of an implication) in the premise of \rref{LR'-Arr}.
 The alternate presentation can be interpreted as a function
-match on the term and the type and returning the conjunction of its premises,
+matching on the term and the type and returning the conjunction of its premises,
 but I wanted to use a mutually defined inductive definition.
 
 \begin{figure}[H]
@@ -328,7 +328,7 @@ determinism, which states that the interpretation indeed behaves like a function
 from types to sets of terms;
 and backward closure, which states that the interpretations of computation types
 are backward closed under multi-step head reduction.
-The last property is why \rref{LR'-F-var} needs to include
+The last property is why \rref{LR-F} needs to include
 computations that \emph{reduce to} strongly neutral terms or returns,
 not merely ones that are such terms.
 
@@ -352,7 +352,7 @@ not merely ones that are such terms.
 
 \begin{proof}
   By mutual induction on the first derivations of the logical relation,
-  then by cases on the second derivations.
+  then by cases on the second.
 \end{proof}
 
 \begin{lemma}[Backward closure] \label{lem:closure}
@@ -361,7 +361,8 @@ not merely ones that are such terms.
 \end{lemma}
 
 \begin{proof}
-  By induction on the derivation of the logical relation.
+  By induction on the derivation of the logical relation,
+  using \rref{SRs-Trans',SRs-App}.
 \end{proof}
 
 The final key property is adequacy,
@@ -407,15 +408,14 @@ semantically well formed with respect to a context.
 
 \begin{definition}[Semantic well-formedness of substitutions]
   A substitution $[[s]]$ is well formed with respect to a context $[[G]]$,
-  written $[[G ⊧ s]]$, if for every $[[x : A ∈ G]]$ and $[[⟦A⟧ ↘ P]]$,
+  written \fbox{$[[G ⊧ s]]$}, if for every $[[x : A ∈ G]]$ and $[[⟦A⟧ ↘ P]]$,
   we have $[[x{s} ∈ P]]$.
   In short, the substitution maps variables in the context
   to values in the interpretations of their types.
 \end{definition}
 
 These judgements can be built up inductively,
-as demonstrated by the below admissible rules,
-which are proven by cases.
+as demonstrated by the below admissible rules.
 
 {\mprset{fraction={-~}{-~}{-}}
 \drules[S]{$[[G ⊧ s]]$}{admissible semantic substitution well-formedness}{Nil,Cons}
@@ -427,10 +427,10 @@ using semantic well formedness of substitutions to handle the context.
 \begin{definition}[Semantic typing]
   \begin{enumerate}[rightmargin=\leftmargin] \leavevmode
     \item $[[v]]$ semantically has type $[[A]]$ under context $[[G]]$,
-      written $[[G ⊧ v : A]]$, if for every $[[s]]$ such that $[[G ⊧ s]]$,
+      written \fbox{$[[G ⊧ v : A]]$}, if for every $[[s]]$ such that $[[G ⊧ s]]$,
       there exists an interpretation $[[⟦A⟧ ↘ P]]$ such that $[[v{s} ∈ P]]$.
     \item $[[m]]$ semantically has type $[[B]]$ under context $[[G]]$,
-      written $[[G ⊧ m : B]]$, if for every $[[s]]$ such that $[[G ⊧ s]]$,
+      written \fbox{$[[G ⊧ m : B]]$}, if for every $[[s]]$ such that $[[G ⊧ s]]$,
       there exists an interpretation $[[⟦B⟧ ↘ P]]$ such that $[[m{s} ∈ P]]$.
   \end{enumerate}
 \end{definition}
@@ -444,7 +444,7 @@ Normalization holds as a corollary.
 
 {\mprset{fraction={-~}{-~}{-}}
 \drules[S]{$[[G ⊧ v : A]]$}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk}
-\drules[S]{$[[G ⊧ m : B]]$}{admissible semantic computation typing}{Force,Arr,App,Ret,Let,Case}
+\drules[S]{$[[G ⊧ m : B]]$}{admissible semantic computation typing}{Force,Lam,App,Ret,Let,Case}
 }
 
 \begin{proof}
@@ -509,16 +509,18 @@ with respect to a traditional presentation of strongly normal terms
 based on full small-step reduction \fbox{$[[v ⇝ w]]$}, \fbox{$[[m ⇝ n]]$} of values and computations.
 I omit here the definitions of these reductions,
 but they encompass all $\beta$-reduction rules and are congruent over all subterms,
-including under binders.
-Traditional strongly normal terms, written $[[v ∈ sn]]$, $[[m ∈ sn]]$,
+including under binders,
+with \fbox{$[[v ⇝* w]]$}, \fbox{$[[m ⇝* n]]$} denoting their reflexive, transitive closures.
+
+Traditional strongly normal terms, defined below,
 are accessibility relations with respect to small-step reduction.
 Terms are inductively defined as strongly normal if they step to strongly normal terms,
 so terms which don't step are trivially normal.
-This rules out looping and diverging terms, since they never stop stepping.
+This rules out diverging terms, since they never stop stepping.
 %
-% \drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normalizing terms}{Val,Com}
+% \drules[sn]{$[[v ∈ sn]], [[m ∈ sn]]$}{strongly normal terms}{Val,Com}
 \begin{mathpar}
-\fbox{$[[v ∈ sn]]$} \quad \fbox{$[[m ∈ sn]]$} \hfill \textit{strongly normalizing terms} \\
+\fbox{$[[v ∈ sn]]$} \quad \fbox{$[[m ∈ sn]]$} \hfill \textit{strongly normal terms} \\
 \drule[]{sn-Val}
 \drule[]{sn-Com}
 \end{mathpar}
@@ -544,13 +546,13 @@ The strategy is to mirror the inductive characterization,
 and define corresponding notions of neutral terms and head reduction,
 with strongly neutral terms being those both neutral and strongly normal.
 As before, variables are the only neutral value,
-but we write $[[v ∈ ne]]$ to say that $[[v]]$ is a variable for symmetry.
+but we write \fbox{$[[v ∈ ne]]$} to say that $[[v]]$ is a variable for symmetry.
 
 \drules[sr]{$[[m ⤳' n]]$}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
 \drules[ne]{$[[m ∈ ne]]$}{neutral computations}{Force,App,Let,Case}
 
 \begin{definition}[Strongly neutral computations]
-  A strongly neutral computation, written $[[m ∈ sne]]$,
+  A strongly neutral computation, written \fbox{$[[m ∈ sne]]$},
   is a computation that is both neutral and strongly normalizing,
   \ie $[[m ∈ ne]]$ and $[[m ∈ sn]]$.
 \end{definition}
@@ -616,7 +618,7 @@ we first need antisubstitution to be able to undo substitutions.
   \Rref{sn-Force-Thunk} holds directly by induction on the premise;
   the remaining proofs are more complex.
   First, given the premise $[[m{x ↦ v} ∈ sn]]$ (or $[[n{z ↦ v}]]$),
-  use \nameref{lem:antisubst-sn} to obtain $[[m ∈ sn]]$.
+  use \nameref{lem:antisubst-sn} to obtain $[[m ∈ sn]]$ (or $[[n ∈ sn]]$).
   Then proceed by double (or triple) induction on the derivations of
   $[[v ∈ sn]]$ and $[[m ∈ sn]]$ (and $[[n ∈ sn]]$ for the case rules).
   Similarly to the admissible strongly normal rules,
@@ -635,7 +637,7 @@ of the structure of both reductions.
 \begin{lemma}[Commutativity] \label{lem:commute}
   If $[[m ⇝ n1]]$ and $[[m ⤳' n2]]$, then either $[[n1]] = [[n2]]$,
   or there exists some $[[m']]$ such that
-  $[[n1 ⤳' m']]$ and $[[n2 ⇝ m']]$.
+  $[[n1 ⤳' m']]$ and $[[n2 ⇝* m']]$.
 \end{lemma}
 
 \begin{proof}
@@ -676,7 +678,7 @@ All of these lemmas at last give us backward closure.
 
 \begin{proof}
   By induction on the derivation of $[[m ⤳' n]]$.
-  The cases correspond exactly to each of
+  The cases correspond exactly to
   \rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}.
 \end{proof}
 
@@ -892,8 +894,9 @@ their typing judgements (2), the logical relation (2),
 the small-step reduction relation (2),
 and the mutually inductive definition of strongly neutral and normal terms and head reduction (4).
 The tactic was used for every proof by mutual induction mentioned here.
-Additionally, it was used twice for single induction
-(\ie all other motives are trivial): \rref{SN-Force-inv} and \nameref{cor:ext}.
+Additionally, it was used thrice for single induction
+(\ie all other motives are trivial):
+\rref{SN-Force-inv}, \nameref{cor:ext}, and \nameref{lem:closure}.
 
 Because the mutual induction tactic is merely a tactic and not a top-level construct,
 some amount of manipulation is still required to massage the proof state
diff --git a/cbpv.ott b/cbpv.ott
index e5e4884..eb88085 100644
--- a/cbpv.ott
+++ b/cbpv.ott
@@ -430,7 +430,7 @@ G ⊧ v : U B
 G ⊧ force v : B
 
 G, x : A ⊧ m : B
------------------ :: Arr
+----------------- :: Lam
 G ⊧ λx. m : A → B
 
 G ⊧ m : A → B
@@ -683,11 +683,10 @@ n ∈ sn
 -------------- :: Let
 let x m n ∈ sn
 
-v ∈ sne
 m ∈ sn
 n ∈ sn
 ----------------------- :: Case
-case v | y.m | z.n ∈ sn
+case x | y.m | z.n ∈ sn
 
 defn
   m ⤳' n :: :: sr :: 'sr_'
diff --git a/cbpv.pdf b/cbpv.pdf
index 6a4dad5..18e9590 100644
--- a/cbpv.pdf
+++ b/cbpv.pdf
@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:1d38a183dd4de5d3f499bfe79d7df72db22a03c8de0457260993998a64d20945
-size 326426
+oid sha256:7524bf83211e81eebb1b2b53487d46a1255122a95492499cd24b1c7631a02694
+size 326980
diff --git a/cbpv.tex b/cbpv.tex
index 4e8e0db..c03ed34 100644
--- a/cbpv.tex
+++ b/cbpv.tex
@@ -173,7 +173,7 @@ Because we're dealing with CBPV, values have no $\beta$ reductions,
 so there's no need for head reduction of values as there are no heads.
 Furthermore, there is only one strongly neutral value,
 so we inline the definition as a variable where needed,
-but also write it as $ \ottnt{v}  \in \kw{SNe} $ for symmetry as appropriate.
+but also write it as \fbox{$ \ottnt{v}  \in \kw{SNe} $} for symmetry as appropriate.
 Otherwise, the remaining four judgements are defined mutually below.
 
 \drules[SNe]{$ \ottnt{m}  \in \kw{SNe} $}{strongly neutral computations}{Force,App,Let,Case}
@@ -288,7 +288,7 @@ but the alternate choices likely work as well.
     or right injections whose values are in that of $\ottnt{A_{{\mathrm{2}}}}$.
   \item Computations in the interpretation of the $ \kw{F} \gap  \ottnt{A} $ type
     reduce to either a neutral computation
-    or a return whose value is in the interpretation of $\ottnt{A}$.
+    or a returned value in the interpretation of $\ottnt{A}$.
   \item Computations are in the interpretation of the function type $ \ottnt{A}  \rightarrow  \ottnt{B} $
     if applying them to values in the interpretation of $\ottnt{A}$
     yields computations in the interpretation of $\ottnt{B}$.
@@ -301,7 +301,7 @@ Unfortunately, this is not well defined,
 since the logical relation appears in a negative position
 (to the left of an implication) in the premise of \rref{LR'-Arr}.
 The alternate presentation can be interpreted as a function
-match on the term and the type and returning the conjunction of its premises,
+matching on the term and the type and returning the conjunction of its premises,
 but I wanted to use a mutually defined inductive definition.
 
 \begin{figure}[H]
@@ -328,7 +328,7 @@ determinism, which states that the interpretation indeed behaves like a function
 from types to sets of terms;
 and backward closure, which states that the interpretations of computation types
 are backward closed under multi-step head reduction.
-The last property is why \rref{LR'-F-var} needs to include
+The last property is why \rref{LR-F} needs to include
 computations that \emph{reduce to} strongly neutral terms or returns,
 not merely ones that are such terms.
 
@@ -352,7 +352,7 @@ not merely ones that are such terms.
 
 \begin{proof}
   By mutual induction on the first derivations of the logical relation,
-  then by cases on the second derivations.
+  then by cases on the second.
 \end{proof}
 
 \begin{lemma}[Backward closure] \label{lem:closure}
@@ -361,7 +361,8 @@ not merely ones that are such terms.
 \end{lemma}
 
 \begin{proof}
-  By induction on the derivation of the logical relation.
+  By induction on the derivation of the logical relation,
+  using \rref{SRs-Trans',SRs-App}.
 \end{proof}
 
 The final key property is adequacy,
@@ -407,15 +408,14 @@ semantically well formed with respect to a context.
 
 \begin{definition}[Semantic well-formedness of substitutions]
   A substitution $\sigma$ is well formed with respect to a context $\Gamma$,
-  written $ \Gamma  \vDash  \sigma $, if for every $ \ottmv{x}  :  \ottnt{A}  \in  \Gamma $ and $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $,
+  written \fbox{$ \Gamma  \vDash  \sigma $}, if for every $ \ottmv{x}  :  \ottnt{A}  \in  \Gamma $ and $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $,
   we have $  \ottmv{x} [  \sigma  ]   \in  \ottnt{P} $.
   In short, the substitution maps variables in the context
   to values in the interpretations of their types.
 \end{definition}
 
 These judgements can be built up inductively,
-as demonstrated by the below admissible rules,
-which are proven by cases.
+as demonstrated by the below admissible rules.
 
 {\mprset{fraction={-~}{-~}{-}}
 \drules[S]{$ \Gamma  \vDash  \sigma $}{admissible semantic substitution well-formedness}{Nil,Cons}
@@ -427,10 +427,10 @@ using semantic well formedness of substitutions to handle the context.
 \begin{definition}[Semantic typing]
   \begin{enumerate}[rightmargin=\leftmargin] \leavevmode
     \item $\ottnt{v}$ semantically has type $\ottnt{A}$ under context $\Gamma$,
-      written $ \Gamma  \vDash  \ottnt{v}  :  \ottnt{A} $, if for every $\sigma$ such that $ \Gamma  \vDash  \sigma $,
+      written \fbox{$ \Gamma  \vDash  \ottnt{v}  :  \ottnt{A} $}, if for every $\sigma$ such that $ \Gamma  \vDash  \sigma $,
       there exists an interpretation $ \mathopen{\llbracket}  \ottnt{A}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ such that $  \ottnt{v} [  \sigma  ]   \in  \ottnt{P} $.
     \item $\ottnt{m}$ semantically has type $\ottnt{B}$ under context $\Gamma$,
-      written $ \Gamma  \vDash  \ottnt{m}  :  \ottnt{B} $, if for every $\sigma$ such that $ \Gamma  \vDash  \sigma $,
+      written \fbox{$ \Gamma  \vDash  \ottnt{m}  :  \ottnt{B} $}, if for every $\sigma$ such that $ \Gamma  \vDash  \sigma $,
       there exists an interpretation $ \mathopen{\llbracket}  \ottnt{B}  \mathclose{\rrbracket} \searrow  \ottnt{P} $ such that $  \ottnt{m} [  \sigma  ]   \in  \ottnt{P} $.
   \end{enumerate}
 \end{definition}
@@ -444,7 +444,7 @@ Normalization holds as a corollary.
 
 {\mprset{fraction={-~}{-~}{-}}
 \drules[S]{$ \Gamma  \vDash  \ottnt{v}  :  \ottnt{A} $}{admissible semantic value typing}{Var,Unit,Inl,Inr,Thunk}
-\drules[S]{$ \Gamma  \vDash  \ottnt{m}  :  \ottnt{B} $}{admissible semantic computation typing}{Force,Arr,App,Ret,Let,Case}
+\drules[S]{$ \Gamma  \vDash  \ottnt{m}  :  \ottnt{B} $}{admissible semantic computation typing}{Force,Lam,App,Ret,Let,Case}
 }
 
 \begin{proof}
@@ -509,16 +509,18 @@ with respect to a traditional presentation of strongly normal terms
 based on full small-step reduction \fbox{$ \ottnt{v}  \rightsquigarrow  \ottnt{w} $}, \fbox{$ \ottnt{m}  \rightsquigarrow  \ottnt{n} $} of values and computations.
 I omit here the definitions of these reductions,
 but they encompass all $\beta$-reduction rules and are congruent over all subterms,
-including under binders.
-Traditional strongly normal terms, written $ \ottnt{v}  \in \kw{sn} $, $ \ottnt{m}  \in \kw{sn} $,
+including under binders,
+with \fbox{$ \ottnt{v}  \rightsquigarrow^*  \ottnt{w} $}, \fbox{$ \ottnt{m}  \rightsquigarrow^*  \ottnt{n} $} denoting their reflexive, transitive closures.
+
+Traditional strongly normal terms, defined below,
 are accessibility relations with respect to small-step reduction.
 Terms are inductively defined as strongly normal if they step to strongly normal terms,
 so terms which don't step are trivially normal.
-This rules out looping and diverging terms, since they never stop stepping.
+This rules out diverging terms, since they never stop stepping.
 %
-% \drules[sn]{$ \ottnt{v}  \in \kw{sn} ,  \ottnt{m}  \in \kw{sn} $}{strongly normalizing terms}{Val,Com}
+% \drules[sn]{$ \ottnt{v}  \in \kw{sn} ,  \ottnt{m}  \in \kw{sn} $}{strongly normal terms}{Val,Com}
 \begin{mathpar}
-\fbox{$ \ottnt{v}  \in \kw{sn} $} \quad \fbox{$ \ottnt{m}  \in \kw{sn} $} \hfill \textit{strongly normalizing terms} \\
+\fbox{$ \ottnt{v}  \in \kw{sn} $} \quad \fbox{$ \ottnt{m}  \in \kw{sn} $} \hfill \textit{strongly normal terms} \\
 \drule[]{sn-Val}
 \drule[]{sn-Com}
 \end{mathpar}
@@ -544,13 +546,13 @@ The strategy is to mirror the inductive characterization,
 and define corresponding notions of neutral terms and head reduction,
 with strongly neutral terms being those both neutral and strongly normal.
 As before, variables are the only neutral value,
-but we write $ \ottnt{v}  \in \kw{ne} $ to say that $\ottnt{v}$ is a variable for symmetry.
+but we write \fbox{$ \ottnt{v}  \in \kw{ne} $} to say that $\ottnt{v}$ is a variable for symmetry.
 
 \drules[sr]{$ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n} $}{strong head reduction}{Thunk,Lam,Ret,Inl,Inr,App,Let}
 \drules[ne]{$ \ottnt{m}  \in \kw{ne} $}{neutral computations}{Force,App,Let,Case}
 
 \begin{definition}[Strongly neutral computations]
-  A strongly neutral computation, written $ \ottnt{m}  \in \kw{sne} $,
+  A strongly neutral computation, written \fbox{$ \ottnt{m}  \in \kw{sne} $},
   is a computation that is both neutral and strongly normalizing,
   \ie $ \ottnt{m}  \in \kw{ne} $ and $ \ottnt{m}  \in \kw{sn} $.
 \end{definition}
@@ -616,7 +618,7 @@ we first need antisubstitution to be able to undo substitutions.
   \Rref{sn-Force-Thunk} holds directly by induction on the premise;
   the remaining proofs are more complex.
   First, given the premise $  \ottnt{m} [   \ottmv{x}  \mapsto  \ottnt{v}   ]   \in \kw{sn} $ (or $ \ottnt{n} [   \ottmv{z}  \mapsto  \ottnt{v}   ] $),
-  use \nameref{lem:antisubst-sn} to obtain $ \ottnt{m}  \in \kw{sn} $.
+  use \nameref{lem:antisubst-sn} to obtain $ \ottnt{m}  \in \kw{sn} $ (or $ \ottnt{n}  \in \kw{sn} $).
   Then proceed by double (or triple) induction on the derivations of
   $ \ottnt{v}  \in \kw{sn} $ and $ \ottnt{m}  \in \kw{sn} $ (and $ \ottnt{n}  \in \kw{sn} $ for the case rules).
   Similarly to the admissible strongly normal rules,
@@ -635,7 +637,7 @@ of the structure of both reductions.
 \begin{lemma}[Commutativity] \label{lem:commute}
   If $ \ottnt{m}  \rightsquigarrow  \ottnt{n_{{\mathrm{1}}}} $ and $ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n_{{\mathrm{2}}}} $, then either $\ottnt{n_{{\mathrm{1}}}} = \ottnt{n_{{\mathrm{2}}}}$,
   or there exists some $\ottnt{m'}$ such that
-  $ \ottnt{n_{{\mathrm{1}}}}  \leadsto_{ \kw{sn} }  \ottnt{m'} $ and $ \ottnt{n_{{\mathrm{2}}}}  \rightsquigarrow  \ottnt{m'} $.
+  $ \ottnt{n_{{\mathrm{1}}}}  \leadsto_{ \kw{sn} }  \ottnt{m'} $ and $ \ottnt{n_{{\mathrm{2}}}}  \rightsquigarrow^*  \ottnt{m'} $.
 \end{lemma}
 
 \begin{proof}
@@ -676,7 +678,7 @@ All of these lemmas at last give us backward closure.
 
 \begin{proof}
   By induction on the derivation of $ \ottnt{m}  \leadsto_{ \kw{sn} }  \ottnt{n} $.
-  The cases correspond exactly to each of
+  The cases correspond exactly to
   \rref{sn-Force-Thunk,sn-App-Lam,sn-Let-Ret,sn-Case-Inl,sn-Case-Inr,sn-App-bwd,sn-Let-bwd}.
 \end{proof}
 
@@ -892,8 +894,9 @@ their typing judgements (2), the logical relation (2),
 the small-step reduction relation (2),
 and the mutually inductive definition of strongly neutral and normal terms and head reduction (4).
 The tactic was used for every proof by mutual induction mentioned here.
-Additionally, it was used twice for single induction
-(\ie all other motives are trivial): \rref{SN-Force-inv} and \nameref{cor:ext}.
+Additionally, it was used thrice for single induction
+(\ie all other motives are trivial):
+\rref{SN-Force-inv}, \nameref{cor:ext}, and \nameref{lem:closure}.
 
 Because the mutual induction tactic is merely a tactic and not a top-level construct,
 some amount of manipulation is still required to massage the proof state
diff --git a/rules.tex b/rules.tex
index 9b717d1..9c22a13 100644
--- a/rules.tex
+++ b/rules.tex
@@ -627,11 +627,11 @@
 }}
 
 
-\newcommand{\ottdruleSXXArr}[1]{\ottdrule[#1]{%
+\newcommand{\ottdruleSXXLam}[1]{\ottdrule[#1]{%
 \ottpremise{  \Gamma ,  \ottmv{x}  \mathbin{:}  \ottnt{A}   \vDash  \ottnt{m}  :  \ottnt{B} }%
 }{
  \Gamma  \vDash   \lambda  \ottmv{x}  \mathpunct{.}  \ottnt{m}   :   \ottnt{A}  \rightarrow  \ottnt{B}  }{%
-{\ottdrulename{S\_Arr}}{}%
+{\ottdrulename{S\_Lam}}{}%
 }}
 
 
@@ -672,7 +672,7 @@
 
 \newcommand{\ottdefnSemCom}[1]{\begin{ottdefnblock}[#1]{$ \Gamma  \vDash  \ottnt{m}  :  \ottnt{B} $}{}
 \ottusedrule{\ottdruleSXXForce{}}
-\ottusedrule{\ottdruleSXXArr{}}
+\ottusedrule{\ottdruleSXXLam{}}
 \ottusedrule{\ottdruleSXXApp{}}
 \ottusedrule{\ottdruleSXXRet{}}
 \ottusedrule{\ottdruleSXXLet{}}
@@ -1053,11 +1053,10 @@
 
 
 \newcommand{\ottdrulesnXXCase}[1]{\ottdrule[#1]{%
-\ottpremise{ \ottnt{v}  \in \kw{sne} }%
 \ottpremise{ \ottnt{m}  \in \kw{sn} }%
 \ottpremise{ \ottnt{n}  \in \kw{sn} }%
 }{
-  \kw{case} \gap  \ottnt{v}  \gap \kw{of} \gap \lbrace \kw{inl} \gap  \ottmv{y}  \Rightarrow  \ottnt{m}  \mathrel{;} \kw{inr} \gap  \ottmv{z}  \Rightarrow  \ottnt{n}  \rbrace   \in \kw{sn} }{%
+  \kw{case} \gap  \ottmv{x}  \gap \kw{of} \gap \lbrace \kw{inl} \gap  \ottmv{y}  \Rightarrow  \ottnt{m}  \mathrel{;} \kw{inr} \gap  \ottmv{z}  \Rightarrow  \ottnt{n}  \rbrace   \in \kw{sn} }{%
 {\ottdrulename{sn\_Case}}{}%
 }}