diff --git a/docs/constructions.tex b/docs/constructions.tex
index 4dc0a2910c9b7ca43af2de1ac504a1b23e6ba972..eceb03316643585a2ee0c4b72ebe51d8a1645982 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -386,7 +386,7 @@ We first lift the transition relation to $\STSS \times \wp(\STST)$ (implementing
 
 We further define \emph{closed} sets of states (given a particular set of tokens) as well as the \emph{closure} of a set:
 \begin{align*}
-\STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \disj T \land \All s'. s \stsfstep{T} s' \Ra s' \in S \\
+\STSclsd(S, T) \eqdef{}& \All s \in S. \STSL(s) \disj T \land \left(\All s'. s \stsfstep{T} s' \Ra s' \in S\right) \\
 \upclose(S, T) \eqdef{}& \setComp{ s' \in \STSS}{\Exists s \in S. s \stsftrans{T} s' }
 \end{align*}
 
diff --git a/docs/model.tex b/docs/model.tex
index 4b68fda0767138c52113e341aa812060636a91a2..392fd1e914184eaba59dd238ab97fba1d32a83d5 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -109,7 +109,7 @@ $\textdom{wp}$ is defined as the fixed-point of a contractive function.
         \All &\rs_\f, m, \mask_\f, \state. 0 \leq m < n \land \mask \disj \mask_\f \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rs \mtimes \rs_\f} \Ra {}\\
         &(\All\val. \toval(\expr) = \val \Ra \Exists \rsB. m+1 \in \pred(\rsB) \land m+1 \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f}) \land {}\\
         &(\toval(\expr) = \bot \land 0 < m \Ra \red(\expr, \state) \land \All \expr_2, \state_2, \expr_\f. \expr,\state \step \expr_2,\state_2,\expr_\f \Ra {}\\
-        &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rsB \mtimes \rs_\f} \land  m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
+        &\qquad \Exists \rsB_1, \rsB_2. m \in \wsat\state{\mask \cup \mask_\f}{\rsB_1 \mtimes \rsB_2 \mtimes \rs_\f} \land  m \in \textdom{wp}(\mask, \expr_2, \pred)(\rsB_1) \land {}&\\
         &\qquad\qquad (\expr_\f = \bot \lor m \in \textdom{wp}(\top, \expr_\f, \Lam\any.\Lam\any.\mathbb{N})(\rsB_2))
     \end{aligned}} \\
   \textdom{wp}_\mask(\expr, \pred) &\eqdef \mathit{fix}(\textdom{pre-wp})(\mask, \expr, \pred)
diff --git a/prelude/pretty.v b/prelude/pretty.v
index 7637aedf0ec050d3b7d4ce6fbbcc07cfafd96625..661ba9b038b9b3041a4432510be0db94667df28f 100644
--- a/prelude/pretty.v
+++ b/prelude/pretty.v
@@ -32,7 +32,8 @@ Lemma pretty_N_go_step x s :
   = pretty_N_go (x `div` 10) (String (pretty_N_char (x `mod` 10)) s).
 Proof.
   unfold pretty_N_go; intros; destruct (wf_guard 32 N.lt_wf_0 x).
-  unfold pretty_N_go_help; fold pretty_N_go_help.
+  destruct wf_guard. (* this makes coqchk happy. *)
+  unfold pretty_N_go_help at 1; fold pretty_N_go_help.
   by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel.
 Qed.
 Instance pretty_N : Pretty N := λ x, pretty_N_go x ""%string.