diff --git a/cbpv.mng b/cbpv.mng
index 94a151e..63c5d8f 100644
--- a/cbpv.mng
+++ b/cbpv.mng
@@ -40,6 +40,7 @@
 \inputott{rules}
 
 \begin{document}
+
 \maketitle
 
 \section{Introduction}
@@ -144,6 +145,8 @@ which expands the set from normal forms
 to terms which must reduce to normal forms.
 
 The general recipe for defining these for CBPV is as follows:
+
+\clearpage
 \begin{itemize}[rightmargin=\leftmargin]
   \item The only strongly neutral values are variables.
   \item Strongly neutral computations are eliminators
@@ -417,9 +420,10 @@ semantically well formed with respect to a context.
 These judgements can be built up inductively,
 as demonstrated by the below admissible rules.
 
-{\mprset{fraction={-~}{-~}{-}}
+\begingroup
+\mprset{fraction={-~}{-~}{-}}
 \drules[S]{$[[G ⊧ s]]$}{admissible semantic substitution well-formedness}{Nil,Cons}
-}
+\endgroup
 
 Then we can define semantic typing in terms of the logical relation,
 using semantic well formedness of substitutions to handle the context.
@@ -442,10 +446,11 @@ the fundamental theorem of soundness of syntactic typing with respect to semanti
 then follows directly.
 Normalization holds as a corollary.
 
-{\mprset{fraction={-~}{-~}{-}}
+\begingroup
+\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,Lam,App,Ret,Let,Case}
-}
+\endgroup
 
 \begin{proof}
   By construction using prior lemmas,
@@ -573,10 +578,11 @@ Proving them additionally requires showing that small-step reduction preserves n
   By mutual induction on the single-step reductions.
 \end{proof}
 
-{\mprset{fraction={-~}{-~}{-}}
+\begingroup
+\mprset{fraction={-~}{-~}{-}}
 \drules[sn]{$[[v ∈ sn]]$}{admissible strongly normal values}{Var,Unit,Inl,Inr,Thunk}
 \drules[sn]{$[[m ∈ sn]]$}{admissible strongly normal computations}{Lam,Ret,Force,App,Let,Case}
-}
+\endgroup
 
 \begin{proof}
   \Rref{sn-App,sn-Let,sn-Case} are proven by double induction
@@ -610,9 +616,10 @@ we first need antisubstitution to be able to undo substitutions.
   By induction on the derivation of $[[m{x ↦ v} ∈ sn]]$.
 \end{proof}
 
-{\mprset{fraction={-~}{-~}{-}}
+\begingroup
+\mprset{fraction={-~}{-~}{-}}
 \drules[sn]{$[[m ∈ sn]]$}{head expansion}{Force-Thunk,App-Lam,Let-Ret,Case-Inl,Case-Inr}
-}
+\endgroup
 
 \begin{proof}
   \Rref{sn-Force-Thunk} holds directly by induction on the premise;
@@ -645,12 +652,15 @@ of the structure of both reductions.
   then by cases on the derivation of $[[m ⇝ n1]]$.
 \end{proof}
 
+\begingroup
+\setlength{\abovedisplayskip}{0pt}
 \begin{mathpar}
 \mprset{fraction={-~}{-~}{-}}
 \fbox{$[[m ∈ sn]]$} \hfill \textit{backward closure in head position} \\
 \drule[width=0.45\textwidth]{sn-App-bwd}
 \drule[width=0.55\textwidth]{sn-Let-bwd}
 \end{mathpar}
+\endgroup
 
 \begin{proof}
   First, use \rref{sn-App-inv1,sn-App-inv2,sn-Let-inv1,sn-Let-inv2}
diff --git a/cbpv.pdf b/cbpv.pdf
index 64377d9..90003fe 100644
--- a/cbpv.pdf
+++ b/cbpv.pdf
@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:168965f631854952bfb76e480f8671ea55d6b644ac7583b2e3d37d10664e805d
-size 327003
+oid sha256:37d78ebbd46cd625a84b1db684252c4053264b1b567e69a31e4e199b1c7c88f7
+size 326964
diff --git a/cbpv.tex b/cbpv.tex
index ecd5e10..7c75dc0 100644
--- a/cbpv.tex
+++ b/cbpv.tex
@@ -40,6 +40,7 @@
 \inputott{rules}
 
 \begin{document}
+
 \maketitle
 
 \section{Introduction}
@@ -144,6 +145,8 @@ which expands the set from normal forms
 to terms which must reduce to normal forms.
 
 The general recipe for defining these for CBPV is as follows:
+
+\clearpage
 \begin{itemize}[rightmargin=\leftmargin]
   \item The only strongly neutral values are variables.
   \item Strongly neutral computations are eliminators
@@ -417,9 +420,10 @@ semantically well formed with respect to a context.
 These judgements can be built up inductively,
 as demonstrated by the below admissible rules.
 
-{\mprset{fraction={-~}{-~}{-}}
+\begingroup
+\mprset{fraction={-~}{-~}{-}}
 \drules[S]{$ \Gamma  \vDash  \sigma $}{admissible semantic substitution well-formedness}{Nil,Cons}
-}
+\endgroup
 
 Then we can define semantic typing in terms of the logical relation,
 using semantic well formedness of substitutions to handle the context.
@@ -442,10 +446,11 @@ the fundamental theorem of soundness of syntactic typing with respect to semanti
 then follows directly.
 Normalization holds as a corollary.
 
-{\mprset{fraction={-~}{-~}{-}}
+\begingroup
+\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,Lam,App,Ret,Let,Case}
-}
+\endgroup
 
 \begin{proof}
   By construction using prior lemmas,
@@ -573,10 +578,11 @@ Proving them additionally requires showing that small-step reduction preserves n
   By mutual induction on the single-step reductions.
 \end{proof}
 
-{\mprset{fraction={-~}{-~}{-}}
+\begingroup
+\mprset{fraction={-~}{-~}{-}}
 \drules[sn]{$ \ottnt{v}  \in \kw{sn} $}{admissible strongly normal values}{Var,Unit,Inl,Inr,Thunk}
 \drules[sn]{$ \ottnt{m}  \in \kw{sn} $}{admissible strongly normal computations}{Lam,Ret,Force,App,Let,Case}
-}
+\endgroup
 
 \begin{proof}
   \Rref{sn-App,sn-Let,sn-Case} are proven by double induction
@@ -610,9 +616,10 @@ we first need antisubstitution to be able to undo substitutions.
   By induction on the derivation of $  \ottnt{m} [   \ottmv{x}  \mapsto  \ottnt{v}   ]   \in \kw{sn} $.
 \end{proof}
 
-{\mprset{fraction={-~}{-~}{-}}
+\begingroup
+\mprset{fraction={-~}{-~}{-}}
 \drules[sn]{$ \ottnt{m}  \in \kw{sn} $}{head expansion}{Force-Thunk,App-Lam,Let-Ret,Case-Inl,Case-Inr}
-}
+\endgroup
 
 \begin{proof}
   \Rref{sn-Force-Thunk} holds directly by induction on the premise;
@@ -645,12 +652,15 @@ of the structure of both reductions.
   then by cases on the derivation of $ \ottnt{m}  \rightsquigarrow  \ottnt{n_{{\mathrm{1}}}} $.
 \end{proof}
 
+\begingroup
+\setlength{\abovedisplayskip}{0pt}
 \begin{mathpar}
 \mprset{fraction={-~}{-~}{-}}
 \fbox{$ \ottnt{m}  \in \kw{sn} $} \hfill \textit{backward closure in head position} \\
 \drule[width=0.45\textwidth]{sn-App-bwd}
 \drule[width=0.55\textwidth]{sn-Let-bwd}
 \end{mathpar}
+\endgroup
 
 \begin{proof}
   First, use \rref{sn-App-inv1,sn-App-inv2,sn-Let-inv1,sn-Let-inv2}