diff --git a/CHANGELOG.md b/CHANGELOG.md
index b1a338fd536568d2b8566ba0e3e8770b47523097..6526732245f639d5abb206251d105e779c1dd44d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -72,7 +72,7 @@ Coq 8.11 is no longer supported in this version of Iris.
 * Slight change to the `AACC` notation for atomic accessors (which is usually
   only printed, not parsed): added a `,` before `ABORT`, for consistency with `COMM`.
 * Add the lemmas `big_sepM_impl_strong` and `big_sepM_impl_dom_subseteq` that
-  generalize the existing `big_sepM_impl` lemma.
+  generalize the existing `big_sepM_impl` lemma. (by Simon Friis Vindum)
 
 **Changes in `proofmode`:**
 
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 104d0be3c95d20b00c44d0ce8bd3af5725abec79..9e82d6e39b3e8834cde8440d00bdc368185a6afe 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1543,6 +1543,7 @@ Proof.
     rewrite pure_True // left_id // wand_elim_l //.
 Qed.
 
+Lemma big_sepM_impl_dom_subseteq `{Countable K} {A B}
     (Φ : K → A → PROP) (Ψ : K → B → PROP) (m1 : gmap K A) (m2 : gmap K B) :
   dom (gset _) m2 ⊆ dom _ m1 →
   ([∗ map] k↦x ∈ m1, Φ k x) -∗