diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index b97101969425b0f40dc7ca06aa7aafac88a27d16..92312ba12cb5c4d360087d82ecd0dd4630a69417 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -267,6 +267,9 @@ Section gmap.
   Lemma big_opM_lookup f m i x :
     m !! i = Some x → f i x ≼ [⋅ map] k↦y ∈ m, f k y.
   Proof. intros. rewrite big_opM_delete //. apply cmra_included_l. Qed.
+  Lemma big_opM_lookup_dom (f : K → M) m i :
+    is_Some (m !! i) → f i ≼ [⋅ map] k↦_ ∈ m, f k.
+  Proof. intros [x ?]. by eapply (big_opM_lookup (λ i x, f i)). Qed.
 
   Lemma big_opM_singleton f i x : ([⋅ map] k↦y ∈ {[i:=x]}, f k y) ≡ f i x.
   Proof.
diff --git a/base_logic/big_op.v b/base_logic/big_op.v
index 0a9b4b59deed4ea6080ee47b13702ba29d20cfcd..40a0a71f2a568df69937f8736c629c21cff3bbfe 100644
--- a/base_logic/big_op.v
+++ b/base_logic/big_op.v
@@ -330,6 +330,9 @@ Section gmap.
   Lemma big_sepM_lookup Φ m i x :
     m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
   Proof. intros. apply uPred_included. by apply: big_opM_lookup. Qed. 
+  Lemma big_sepM_lookup_dom (Φ : K → uPred M) m i :
+    is_Some (m !! i) → ([∗ map] k↦_ ∈ m, Φ k) ⊢ Φ i.
+  Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
 
   Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
   Proof. by rewrite big_opM_singleton. Qed.