diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
index 9012c2f449808d7472da82f34aef11b94487d9a4..3b3cf03ba3c35e79502655ef801e348c136dd6d0 100644
--- a/tests/multiset_solver.v
+++ b/tests/multiset_solver.v
@@ -66,4 +66,8 @@ Section test.
       {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊎
       {[ x5 ]} ⊎ {[ x5 ]} ⊎ {[ x6 ]} ⊎ {[ x7 ]} ⊎ {[ x9 ]} ⊎ {[ x8 ]} ⊎ {[ x8 ]}.
   Proof. multiset_solver. Qed.
+
+  Lemma test_firstorder_1 (P : A → Prop) x X :
+    P x ∧ (∀ y, y ∈ X → P y) ↔ (∀ y, y ∈ {[x]} ⊎ X → P y).
+  Proof. multiset_solver. Qed.
 End test.
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index eb03459718e8d0594d2b0b6f4662142417da1ee7..6dcc63eb4dfc43c7a73cd112e792658490ab3d9d 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -243,7 +243,7 @@ Section multiset_unfold.
     - f_equiv. by apply set_unfold_multiset_subseteq.
   Qed.
   Global Instance set_unfold_multiset_elem_of X x n :
-    MultisetUnfold x X n → SetUnfold (x ∈ X) (0 < n) | 0.
+    MultisetUnfold x X n → SetUnfoldElemOf x X (0 < n) | 100.
   Proof. constructor. by rewrite <-(multiset_unfold x X n). Qed.
 End multiset_unfold.