diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
index 3b3cf03ba3c35e79502655ef801e348c136dd6d0..64bc0951026d9be664270882b74237c13ddbc78a 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 :