From 3375dd20fe9869ffd996d881398f1319e346d241 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Mar 2021 08:51:42 +0100
Subject: [PATCH] =?UTF-8?q?Turn=20`x=20=E2=88=88=20X`=20only=20into=20`0?=
 =?UTF-8?q?=20<=20multiplicity=20x=20X`=20at=20leaves=20of=20`=E2=88=88`?=
 =?UTF-8?q?=20to=20enable=20better=20first-order=20reasoning.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/multiset_solver.v | 4 ++++
 theories/gmultiset.v    | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
index 9012c2f4..3b3cf03b 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 eb034597..6dcc63eb 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.
 
-- 
GitLab