Turn `x ∈ X` only into `0 < multiplicity x X` at leaves of `∈` to enable...

Turn `x ∈ X` only into `0 < multiplicity x X` at leaves of `∈` to enable better first-order reasoning.

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.

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.