diff --git a/CHANGELOG.md b/CHANGELOG.md
index 516c417e0685b50c84f93f8f63eebf310764ac48..1d6391d9941d325a526ab96c62f12fbcd4545d3a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,7 @@ API-breaking change is listed.
   `elem_of_StronglySorted_app` → `StronglySorted_app_1_elem_of`,
   `StronglySorted_app_inv_l` → `StronglySorted_app_1_l`
   `StronglySorted_app_inv_r` → `StronglySorted_app_1_r`. (by Marijn van Wezel)
+- Add `SetUnfoldElemOf` instance for `dom` on `gmultiset`. (by Marijn van Wezel)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
index 0f0e4beef94616ff56e08ce770dce193a43a39c2..2b3db9e012a64efd92121fb084ce42df3998e520 100644
--- a/tests/multiset_solver.v
+++ b/tests/multiset_solver.v
@@ -58,6 +58,9 @@ Section test.
   Lemma test_elem_of_6 x y X : {[+ x; y +]} ⊆ X → x ∈ X ∧ y ∈ X.
   Proof. multiset_solver. Qed.
 
+  Lemma test_elem_of_dom x X : x ∈ dom X ↔ x ∈ X.
+  Proof. multiset_solver. Qed.
+
   (** Tests where the goals do not involve the multiset connectives *)
   Lemma test_goal_1 x y X : {[+ x +]} ∪ X ⊆ {[+ y +]} → x = y.
   Proof. multiset_solver. Qed.