From 691a600055373cc9220815bc939d999b087d23e7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Mar 2021 08:21:31 +0100
Subject: [PATCH] =?UTF-8?q?Better=20tests=20for=20`=E2=88=88`=20in=20concl?=
 =?UTF-8?q?usion=20of=20`multiset=5Fsolver`=20goal.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 tests/multiset_solver.v | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
index 3b3cf03b..64bc0951 100644
--- a/tests/multiset_solver.v
+++ b/tests/multiset_solver.v
@@ -33,13 +33,17 @@ Section test.
     multiplicity x X < 3 → {[ x ]} ⊎ {[ x ]} ⊎ {[ x ]} ⊈ X.
   Proof. multiset_solver. Qed.
 
-  Lemma test_elem_of_1 x X : x ∈ X → {[x]} ⊆ X.
+  Lemma test_elem_of_1 x X : x ∈ X ↔ {[x]} ⊎ ∅ ⊆ X.
   Proof. multiset_solver. Qed.
-  Lemma test_elem_of_2 x y X : x ≠ y → x ∈ X → y ∈ X → {[x]} ⊎ {[y]} ⊆ X.
+  Lemma test_elem_of_2 x X : x ∈ X ↔ {[x]} ∪ ∅ ⊆ X.
   Proof. multiset_solver. Qed.
-  Lemma test_elem_of_3 x y X Y : x ≠ y → x ∈ X → y ∈ Y → {[x]} ⊎ {[y]} ⊆ X ∪ Y.
+  Lemma test_elem_of_3 x y X : x ≠ y → x ∈ X → y ∈ X → {[x]} ⊎ {[y]} ⊆ X.
   Proof. multiset_solver. Qed.
-  Lemma test_elem_of_4 x y X Y : x ≠ y → x ∈ X → y ∈ Y → {[x]} ⊆ (X ∪ Y) ∖ {[ y ]}.
+  Lemma test_elem_of_4 x y X Y : x ≠ y → x ∈ X → y ∈ Y → {[x]} ⊎ {[y]} ⊆ X ∪ Y.
+  Proof. multiset_solver. Qed.
+  Lemma test_elem_of_5 x y X Y : x ≠ y → x ∈ X → y ∈ Y → {[x]} ⊆ (X ∪ Y) ∖ {[ y ]}.
+  Proof. multiset_solver. Qed.
+  Lemma test_elem_of_6 x y X : {[x]} ⊎ {[y]} ⊆ X → x ∈ X ∧ y ∈ X.
   Proof. multiset_solver. Qed.
 
   Lemma test_big_1 x1 x2 x3 x4 :
-- 
GitLab