Put `SetUnfoldElemOf` instances together.

theories/gmultiset.v

@@ -133,14 +133,6 @@ Section basic_lemmas.
 
   Lemma gmultiset_elem_of_disj_union X Y x : x ∈ X ⊎ Y ↔ x ∈ X ∨ x ∈ Y.
   Proof. rewrite !elem_of_multiplicity, multiplicity_disj_union. lia. Qed.
-
-  Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
-    SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
-    SetUnfoldElemOf x (X ⊎ Y) (P ∨ Q).
-  Proof.
-    intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
-    by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q).
-  Qed.
 End basic_lemmas.
 
 (** * A solver for multisets *)
@@ -242,9 +234,17 @@ Section multiset_unfold.
     - by apply set_unfold_multiset_subseteq.
     - f_equiv. by apply set_unfold_multiset_subseteq.
   Qed.
+
   Global Instance set_unfold_multiset_elem_of X x n :
     MultisetUnfold x X n → SetUnfoldElemOf x X (0 < n) | 100.
   Proof. constructor. by rewrite <-(multiset_unfold x X n). Qed.
+  Global Instance set_unfold_gmultiset_disj_union x X Y P Q :
+    SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
+    SetUnfoldElemOf x (X ⊎ Y) (P ∨ Q).
+  Proof.
+    intros ??; constructor. rewrite gmultiset_elem_of_disj_union.
+    by rewrite <-(set_unfold_elem_of x X P), <-(set_unfold_elem_of x Y Q).
+  Qed.
 End multiset_unfold.
 
 (** Step 3: instantiate hypotheses *)