diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index afdb923321b0b51a64ecb2edd8424a89a4aff115..2dfb4a3d7e4186bfd9d29efd6d2a54de6155b163 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1524,25 +1524,13 @@ 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.
+  Lemma Some_includedN_opM 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.
+    rewrite /includedN. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
   Qed.
-  Lemma Some_included_alt a b : Some a ≼ Some b ↔ ∃ mc, b ≡ a ⋅? mc.
+  Lemma Some_included_opM 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.
+    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.
diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index 429e93e5b1a4aa8a61495de4c23f202c8d426d2c..9c722d4d8c08581427b6300b5835c950cd28976d 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -84,7 +84,7 @@ Section updates.
     - apply (cmra_validN_le n); last lia.
       move: Hmz; rewrite Hz. destruct mz; simpl; eauto using cmra_validN_op_l.
     - eapply (cmra_includedN_le n); last lia.
-      apply Some_includedN_alt. eauto.
+      apply Some_includedN_opM. eauto.
   Qed.
   Lemma local_update_valid `{!CmraDiscrete A} x y x' y' :
     (✓ x → ✓ y → Some y ≼ Some x → (x,y) ~l~> (x',y')) → (x,y) ~l~> (x',y').