diff --git a/cbpv.mng b/cbpv.mng
index 1bbd6c9..5ed10dc 100644
--- a/cbpv.mng
+++ b/cbpv.mng
@@ -505,7 +505,7 @@ and it doesn't describe reducing anywhere other than in the head position.
 
 The solution we take from POPLMark Reloaded is to prove that $\kw{SN}$ is sound
 with respect to a traditional presentation of strongly normal terms
-based on full small-step reduction $[[v ⇝ w]]$, $[[m ⇝ n]]$ of values and computations.
+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.
diff --git a/cbpv.pdf b/cbpv.pdf
index 2e35f6f..c4d2293 100644
--- a/cbpv.pdf
+++ b/cbpv.pdf
@@ -1,3 +1,3 @@
 version https://git-lfs.github.com/spec/v1
-oid sha256:a31aa4f3d423add5b5ce1d9b7ae67baa176cb9d1bcd7cd496993c6227e78fd4b
-size 325048
+oid sha256:3f9ad844241135ba18c1223004db36ab7dde032d8da90a76e1187f8ede357d46
+size 325129
diff --git a/cbpv.tex b/cbpv.tex
index 3646e75..9953df2 100644
--- a/cbpv.tex
+++ b/cbpv.tex
@@ -505,7 +505,7 @@ and it doesn't describe reducing anywhere other than in the head position.
 
 The solution we take from POPLMark Reloaded is to prove that $\kw{SN}$ is sound
 with respect to a traditional presentation of strongly normal terms
-based on full small-step reduction $ \ottnt{v}  \rightsquigarrow  \ottnt{w} $, $ \ottnt{m}  \rightsquigarrow  \ottnt{n} $ of values and computations.
+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.