From 891f58bfecbb65d8382f17ae5f277b42c95608dd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Mar 2021 10:45:11 +0100
Subject: [PATCH] Put `SetUnfoldElemOf` instances together.

---
 theories/gmultiset.v | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 6dcc63eb..1b4a1568 100644
--- a/theories/gmultiset.v
+++ b/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 *)
-- 
GitLab