diff --git a/docs/proof_guide.md b/docs/proof_guide.md
index b07e06df8528958adcb004fd3ad24d84db054888..8de11312949df0bc65e4531a0e40957536d02f1c 100644
--- a/docs/proof_guide.md
+++ b/docs/proof_guide.md
@@ -295,10 +295,13 @@ their default level (`200`).
 
 Moreover, correct parsing of notations sometimes relies on Coq's automatic
 left-factoring, which can require coordinating levels of certain "conflicting"
-notations and their subexpressions. For instance, to disambiguate `(⊢@{ PROP })`
-and `(⊢@{ PROP } P)`, Coq must factor out a nonterminal for `⊢@{ PROP }`, but it
-can only do so if all occurrences of `⊢@{ PROP }` agree on the precedences for
-all subexpressions.
+notations and their subexpressions.  For instance, to disambiguate `(⊢@{ PROP
+})` and `(⊢@{ PROP } P)`, Coq must factor out a nonterminal for `⊢@{ PROP }`,
+but it can only do so if all occurrences of `⊢@{ PROP }` agree on the
+precedences for all subexpressions. This also requires using the same
+tokenization in all cases, i.e., the notation has to consistently be declared as
+`(⊢@{` or `('⊢@{'`, but not a mixture of the two. The latter form of using
+explicit tokenization with `'` is preferred to avoid relying on Coq's default.
 
 For details, consult [the Coq manual](https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#simple-factorization-rules).