diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 50e46234624fe4e5cb892f1a13e258bc18105ea9..afdb923321b0b51a64ecb2edd8424a89a4aff115 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1524,6 +1524,27 @@ Section option.
   Lemma Some_included_is_Some x mb : Some x ≼ mb → is_Some mb.
   Proof. rewrite option_included. naive_solver. Qed.
 
+  Lemma Some_includedN_alt n a b : Some a ≼{n} Some b ↔ ∃ mc, b ≡{n}≡ a ⋅? mc.
+  Proof.
+    rewrite Some_includedN. split.
+    - intros [Heq|[c Heq]].
+      + exists None. auto.
+      + exists (Some c). auto.
+    - intros [[c|] Heq].
+      + right. exists c. auto.
+      + left. auto.
+  Qed.
+  Lemma Some_included_alt a b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc.
+  Proof.
+    rewrite Some_included. split.
+    - intros [Heq|[c Heq]].
+      + exists None. auto.
+      + exists (Some c). auto.
+    - intros [[c|] Heq].
+      + right. exists c. auto.
+      + left. auto.
+  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.
   Lemma Some_included_total `{!CmraTotal A} a b : Some a ≼ Some b ↔ a ≼ b.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 9e81bb8dfcabda6f4db4ed8f2051d1b70b40df02..1685b9fde8f0a6a547e824e63b1d50253ae174c2 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 dd679d26ff1cade494e850a338e354a670b714e5..429e93e5b1a4aa8a61495de4c23f202c8d426d2c 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_alt. 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].