diff --git a/CHANGELOG.md b/CHANGELOG.md
index d9019babc26e4932e519a3ac468771d64bf9b575..e0cf578f7426a2df2ebeb38ea060415828294468 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -39,6 +39,11 @@ Coq 8.13 is no longer supported.
   (by Michael Sammler, Lennard Gäher, and Simon Spies).
 * Add `max_Z` and `mono_Z` cameras.
 * Add `dfrac_valid`.
+* Rename `Some_included_2` to `Some_included_mono`.
+* Consistently use `Some x ≼ Some y` to express the reflexive closure of
+  `x ≼ y`. This changes the statements of some lemmas: `singleton_included`,
+  `local_update_valid0`, `local_update_valid`. Also add various new
+  `Some_included` lemmas to help deal with these assertions.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 88b3f79ddeb8d19eb7270d232b6573483e6f64dd..d0e87654bf359bdbaf45d007c4fc5f6c2f19de78 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -17,6 +17,9 @@ Notation "(â‹…)" := op (only parsing) : stdpp_scope.
    reflexivity.  However, if we used [option A], the following would no longer
    hold:
      x ≼ y ↔ x.1 ≼ y.1 ∧ x.2 ≼ y.2
+   If you need the reflexive closure of the inclusion relation, you can use
+   [Some a ≼ Some b]. There are various [Some_included] lemmas that help
+   deal with propositions of this shape.
 *)
 Definition included {A} `{!Equiv A, !Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
 Infix "≼" := included (at level 70) : stdpp_scope.
@@ -1414,6 +1417,8 @@ Section option.
     right. exists a, b. by rewrite {3}Hab.
   Qed.
 
+  (* See below for more [included] lemmas. *)
+
   Lemma option_cmra_mixin : CmraMixin (option A).
   Proof.
     apply cmra_total_mixin.
@@ -1501,10 +1506,34 @@ Section option.
 
   Lemma Some_includedN n a b : Some a ≼{n} Some b ↔ a ≡{n}≡ b ∨ a ≼{n} b.
   Proof. rewrite option_includedN; naive_solver. Qed.
+  Lemma Some_includedN_1 n a b : Some a ≼{n} Some b → a ≡{n}≡ b ∨ a ≼{n} b.
+  Proof. rewrite Some_includedN. auto. Qed.
+  Lemma Some_includedN_2 n a b : a ≡{n}≡ b ∨ a ≼{n} b → Some a ≼{n} Some b.
+  Proof. rewrite Some_includedN. auto. Qed.
+  Lemma Some_includedN_mono n a b : a ≼{n} b → Some a ≼{n} Some b.
+  Proof. rewrite Some_includedN. auto. Qed.
+  Lemma Some_includedN_is_Some n x mb : Some x ≼{n} mb → is_Some mb.
+  Proof. rewrite option_includedN. naive_solver. Qed.
+
   Lemma Some_included a b : Some a ≼ Some b ↔ a ≡ b ∨ a ≼ b.
   Proof. rewrite option_included; naive_solver. Qed.
-  Lemma Some_included_2 a b : a ≼ b → Some a ≼ Some b.
-  Proof. rewrite Some_included; eauto. Qed.
+  Lemma Some_included_1 a b : Some a ≼ Some b → a ≡ b ∨ a ≼ b.
+  Proof. rewrite Some_included. auto. Qed.
+  Lemma Some_included_2 a b : a ≡ b ∨ a ≼ b → Some a ≼ Some b.
+  Proof. rewrite Some_included. auto. Qed.
+  Lemma Some_included_mono a b : a ≼ b → Some a ≼ Some b.
+  Proof. rewrite Some_included. auto. Qed.
+  Lemma Some_included_is_Some x mb : Some x ≼ mb → is_Some mb.
+  Proof. rewrite option_included. naive_solver. Qed.
+
+  Lemma Some_includedN_opM n a b : Some a ≼{n} Some b ↔ ∃ mc, b ≡{n}≡ a ⋅? mc.
+  Proof.
+    rewrite /includedN. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
+  Qed.
+  Lemma Some_included_opM a b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc.
+  Proof.
+    rewrite /included. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
+  Qed.
 
   Lemma Some_includedN_total `{!CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
   Proof. rewrite Some_includedN. split; [|by eauto]. by intros [->|?]. Qed.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 126f67a6b8ae21be6d807e7960caea27be4d5768..20d6ae2aa2497132ff8adb36cd0c628e1c1d0fa5 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -361,16 +361,18 @@ Proof.
   intros (y&?&->%(Some_included_exclusive _)); eauto using lookup_valid_Some.
 Qed.
 Lemma singleton_included i x y :
-  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ x ≡ y ∨ x ≼ y.
+  {[ i := x ]} ≼ ({[ i := y ]} : gmap K A) ↔ Some x ≼ Some y.
 Proof.
   rewrite singleton_included_l. split.
-  - intros (y'&Hi&?). rewrite lookup_insert in Hi.
-    apply Some_included. by rewrite Hi.
-  - intros ?. exists y. by rewrite lookup_insert Some_included.
+  - intros (y'&Hi&?). rewrite lookup_insert in Hi. by rewrite Hi.
+  - intros ?. exists y. by rewrite lookup_insert.
 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 :
   x ≼ y → {[ i := x ]} ≼ ({[ i := y ]} : gmap K A).
-Proof. intros Hincl. apply singleton_included. right. done. Qed.
+Proof. intros Hincl. apply singleton_included, Some_included_mono. done. Qed.
 
 Global Instance singleton_cancelable i x :
   Cancelable (Some x) → Cancelable {[ i := x ]}.
diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index 4c28262155795101e97252ab600f2e4aa05fb0fc..13de20bd2b1580d17c875095e9285e77934ebd62 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -76,30 +76,28 @@ Section updates.
   Qed.
 
   Lemma local_update_valid0 x y x' y' :
-    (✓{0} x → ✓{0} y → x ≡{0}≡ y ∨ y ≼{0} x → (x,y) ~l~> (x',y')) →
+    (✓{0} x → ✓{0} y → Some y ≼{0} Some x → (x,y) ~l~> (x',y')) →
     (x,y) ~l~> (x',y').
   Proof.
     intros Hup n mz Hmz Hz; simpl in *. apply Hup; auto.
     - by apply (cmra_validN_le n); last lia.
     - apply (cmra_validN_le n); last lia.
       move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l.
-    - destruct mz as [z|].
-      + right. exists z. apply dist_le with n; auto with lia.
-      + left. apply dist_le with n; auto with lia.
+    - eapply (cmra_includedN_le n); last lia.
+      apply Some_includedN_opM. eauto.
   Qed.
   Lemma local_update_valid `{!CmraDiscrete A} x y x' y' :
-    (✓ x → ✓ y → x ≡ y ∨ y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
+    (✓ x → ✓ y → Some y ≼ Some x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
   Proof.
-    rewrite !(cmra_discrete_valid_iff 0)
-      (cmra_discrete_included_iff 0) (discrete_iff 0).
+    rewrite !(cmra_discrete_valid_iff 0) (cmra_discrete_included_iff 0).
     apply local_update_valid0.
   Qed.
 
   Lemma local_update_total_valid0 `{!CmraTotal A} x y x' y' :
     (✓{0} x → ✓{0} y → y ≼{0} x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
   Proof.
-    intros Hup. apply local_update_valid0=> ?? [Hx|?]; apply Hup; auto.
-    by rewrite Hx.
+    intros Hup. apply local_update_valid0=> ?? Hincl. apply Hup; auto.
+    by apply Some_includedN_total.
   Qed.
   Lemma local_update_total_valid `{!CmraTotal A, !CmraDiscrete A} x y x' y' :
     (✓ x → ✓ y → y ≼ x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').
diff --git a/iris/base_logic/lib/gen_inv_heap.v b/iris/base_logic/lib/gen_inv_heap.v
index 949ff543db28b8705562f02f177be656129f69ee..46d9a715bc43bfc904be9e552bd3c0c200feff44 100644
--- a/iris/base_logic/lib/gen_inv_heap.v
+++ b/iris/base_logic/lib/gen_inv_heap.v
@@ -219,8 +219,9 @@ Section inv_heap.
 
   Lemma inv_mapsto_own_inv l v I : l ↦_I v -∗ l ↦_I □.
   Proof.
-    iApply own_mono. apply auth_frag_mono. rewrite singleton_included pair_included.
-    right. split; [apply: ucmra_unit_least|done].
+    iApply own_mono. apply auth_frag_mono.
+    rewrite singleton_included_total pair_included.
+    split; [apply: ucmra_unit_least|done].
   Qed.
 
   (** An accessor to make use of [inv_mapsto_own].
diff --git a/iris_unstable/algebra/list.v b/iris_unstable/algebra/list.v
index 479f6a97ef3842bd4843f65bdbed421140206df6..47300ee4947f58690dff003cf3aed018d042d3e0 100644
--- a/iris_unstable/algebra/list.v
+++ b/iris_unstable/algebra/list.v
@@ -267,8 +267,8 @@ Section properties.
     - rewrite list_lookup_singletonM_lt //.
       destruct (lookup_lt_is_Some_2 l j) as [z Hz].
       { trans i; eauto using lookup_lt_Some. }
-      rewrite Hz. by apply Some_included_2, ucmra_unit_least.
-    - rewrite list_lookup_singletonM Hi. by apply Some_included_2.
+      rewrite Hz. by apply Some_included_mono, ucmra_unit_least.
+    - rewrite list_lookup_singletonM Hi. by apply Some_included_mono.
     - rewrite list_lookup_singletonM_gt //. apply: ucmra_unit_least.
   Qed.