diff --git a/CHANGELOG.md b/CHANGELOG.md
index 522940facb4d79ced8ee5dec57aa2a8ecac95ed5..82a87f1de7ea3edf64fa6941260e195eff0d2354 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -47,6 +47,7 @@ Coq 8.13 is no longer supported.
 * Add hints for `a ≼ a ⋅ _` / `a ≼ _ ⋅ a` / `ε ≼ _` / `_ ≼ CsumBot` /
   `_ ≼ ExclBot` with cost 0, which means they are used by `done` to finish
   proofs. (by Ike Mulder)
+* Rename `singleton_mono` to `singleton_included_mono`.
 
 **Changes in `bi`:**
 
diff --git a/docs/style_guide.md b/docs/style_guide.md
index 66a069dc8576db8249ab2d6eff2bc1619512bc05..c09039634eb06008bb60e3b7261615c2d505a625 100644
--- a/docs/style_guide.md
+++ b/docs/style_guide.md
@@ -210,10 +210,6 @@ theories/base_logic/lib is for constructions in the base logic (using own)
 * `list_lookup_insert` is named by context (the type involved), then the two functions outside-in on the left-hand-side, so it has the type `lookup (insert …) = …` where the `insert` is on a list. Notations mean it doesn’t actually look like this and the insert is textually first.
 * Injectivity theorems are instances of `Inj` and then are used with `inj`
 * Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant).
-* Entailments at the top level are typically written `P -* Q`, which is notation
-  for `P ⊢ Q`. If you have a theorem which has no premises you have to write ⊢ P
-  explicitly (for example, it is common to have `⊢ |==> ∃ γ, …` for an allocation
-  theorem)
 * Suffix `'` (prime) is used when `foo'` is a corollary of `foo`. Try to avoid
   these since the name doesn't convey how `foo'` is related to `foo`.
 * Given a polymorphic function/relation `f` (e.g., `eq`, `equiv`, `subseteq`), the instance of type `A` is called `A_f_instance`, and we add a lemma `A_f` that characterizes the instance. In case of many instances, this lemma is proved by unfolding the definition of the instance, e.g., `frac_op`, `frac_valid`. However, in some cases, e.g., `list_eq`, `map_eq`, `set_eq` this lemma might require non-trivial proof work.
@@ -224,6 +220,7 @@ theories/base_logic/lib is for constructions in the base logic (using own)
     M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
     M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
     ```
+* Monotonicity lemmas where the relation can be ambiguous are called `<f>_<relation>_mono`, e.g. `Some_included_mono`.
 
 ### Naming algebra libraries
 
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 58ce801bb6489895dcddc960a612b97d5a5e2d7d..ead5b1e596305edf33fbb8dcfd29337e6d6f0230 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -369,7 +369,7 @@ Qed.
 Lemma singleton_included_total `{!CmraTotal A}  i x y :
   {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≼ y.
 Proof. rewrite singleton_included Some_included_total. done. Qed.
-Lemma singleton_mono i x y :
+Lemma singleton_included_mono i x y :
   x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
 Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.