diff --git a/ProofMode.md b/ProofMode.md
index 9d2220a73c379e5d46582ad014348b4de3a5565f..4e8a1599321c85be80a156960f0daffe31d01a2d 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -237,11 +237,13 @@ appear at the top level:
 
 For example, given:
 
-        ∀ x, x = 0 ⊢ □ (P → False ∨ □ (Q ∧ ▷ R) -∗ P ∗ ▷ (R ∗ Q ∧ x = pred 2)).
+        ∀ x, <affine> ⌜ x = 0 ⌝ ⊢
+          □ (P → False ∨ □ (Q ∧ ▷ R) -∗
+          P ∗ ▷ (R ∗ Q ∧ ⌜ x = pred 2 ⌝)).
 
 You can write
 
-        iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
+        iIntros (x Hx) "!# $ [[] | #[HQ HR]] /= !>".
 
 which results in: