More big op lemmas.

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.

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.