diff --git a/CHANGELOG.md b/CHANGELOG.md
index e792007c6013b60b15a5ef99d5346d4f604f66da..64365e8ebb6625e83380d3a9eff03ef5bfb415c5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,16 @@ API-breaking change is listed.
   and `{[ (x,y,z) ]}`. They date back to the time we used the `singleton` class
   with a product for maps (there's now the `singletonM` class).
 - Add map notations `{[ k1 := x1 ; .. ; kn := xn ]}` up to arity 13.
+- Add multiset literal notation `{[+ x1; .. ; xn +]}`.
+  + Add a new type class `SingletonMS` (with projection `{[+ x +]}` for
+    multiset singletons.
+  + Define `{[+ x1; .. ; xn +]}` as notation for `{[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}`.
+- Remove the `Singleton` and `Semiset` instances for multisets to avoid
+  accidental use.
+  + This means the notation `{[ x1; .. ; xn ]}` no longer works for multisets
+    (previously, its definition was wrong, since it used `∪` instead of `⊎`).
+  + Add lemmas for `∈` and `∉` specific for multisets, since the set lemmas no
+    longer work for multisets.
 
 ## std++ 1.5.0
 
diff --git a/tests/multiset_solver.v b/tests/multiset_solver.v
index 64bc0951026d9be664270882b74237c13ddbc78a..511b35870b5de48a798eda0cf214d0b896bdbf2e 100644
--- a/tests/multiset_solver.v
+++ b/tests/multiset_solver.v
@@ -5,73 +5,66 @@ Section test.
   Implicit Types x y : A.
   Implicit Types X Y : gmultiset A.
 
-  Lemma test_eq_1 x y X : {[x]} ⊎ ({[y]} ⊎ X) = {[y]} ⊎ ({[x]} ⊎ X).
+  Lemma test_eq_1 x y X : {[+ x; y +]} ⊎ X = {[+ y; x +]} ⊎ X.
   Proof. multiset_solver. Qed.
   Lemma test_eq_2 x y z X Y :
-    {[z]} ⊎ X = {[y]} ⊎ Y →
-    {[x]} ⊎ ({[z]} ⊎ X) = {[y]} ⊎ ({[x]} ⊎ Y).
+    {[+ z +]} ⊎ X = {[+ y +]} ⊎ Y →
+    {[+ x; z +]} ⊎ X = {[+ y; x +]} ⊎ Y.
   Proof. multiset_solver. Qed.
 
-  Lemma test_neq_1 x y X : {[x]} ⊎ ({[y]} ⊎ X) ≠ ∅.
+  Lemma test_neq_1 x y X : {[+ x; y +]} ⊎ X ≠ ∅.
   Proof. multiset_solver. Qed.
-  Lemma test_neq_2 x : {[x]} ⊎ ∅ ≠@{gmultiset A} ∅.
+  Lemma test_neq_2 x : {[+ x +]} ⊎ ∅ ≠@{gmultiset A} ∅.
   Proof. multiset_solver. Qed.
-  Lemma test_neq_3 X x : X ⊎ ∅ = {[x]} → X ⊎ ∅ ≠@{gmultiset A} ∅.
+  Lemma test_neq_3 X x : X ⊎ ∅ = {[+ x +]} → X ⊎ ∅ ≠@{gmultiset A} ∅.
   Proof. multiset_solver. Qed.
-  Lemma test_neq_4 x y : {[ x ]} ∖ {[ y ]} ≠@{gmultiset A} ∅ → x ≠ y.
+  Lemma test_neq_4 x y : {[+ x +]} ∖ {[+ y +]} ≠@{gmultiset A} ∅ → x ≠ y.
   Proof. multiset_solver. Qed.
-  Lemma test_neq_5 x y Y : y ∈ Y → {[ x ]} ∖ Y ≠ ∅ → x ≠ y.
+  Lemma test_neq_5 x y Y : y ∈ Y → {[+ x +]} ∖ Y ≠ ∅ → x ≠ y.
   Proof. multiset_solver. Qed.
 
   Lemma test_multiplicity_1 x X Y :
     2 < multiplicity x X → X ⊆ Y → 1 < multiplicity x Y.
   Proof. multiset_solver. Qed.
   Lemma test_multiplicity_2 x X :
-    2 < multiplicity x X → {[ x ]} ⊎ {[ x ]} ⊎ {[ x ]} ⊆ X.
+    2 < multiplicity x X → {[+ x; x; x +]} ⊆ X.
   Proof. multiset_solver. Qed.
   Lemma test_multiplicity_3 x X :
-    multiplicity x X < 3 → {[ x ]} ⊎ {[ x ]} ⊎ {[ x ]} ⊈ X.
+    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 X : x ∈ X ↔ {[x]} ∪ ∅ ⊆ X.
+  Lemma test_elem_of_2 x X : x ∈ X ↔ {[+ x +]} ∪ ∅ ⊆ X.
   Proof. multiset_solver. Qed.
-  Lemma test_elem_of_3 x y X : x ≠ y → x ∈ X → y ∈ X → {[x]} ⊎ {[y]} ⊆ X.
+  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]} ⊎ {[y]} ⊆ X ∪ 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 ]}.
+  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.
+  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 :
-    {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊆@{gmultiset A}
-      {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]}.
+    {[+ x1; x2; x3; x4; x4 +]} ⊆@{gmultiset A} {[+ x1; x1; x2; x3; x4; x4 +]}.
   Proof. multiset_solver. Qed.
   Lemma test_big_2 x1 x2 x3 x4 X :
     2 ≤ multiplicity x4 X →
-    {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊆@{gmultiset A}
-      {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ X.
+    {[+ x1; x2; x3; x4; x4 +]} ⊆@{gmultiset A} {[+ x1; x1; x2; x3 +]} ⊎ X.
   Proof. multiset_solver. Qed.
   Lemma test_big_3 x1 x2 x3 x4 X :
     4 ≤ multiplicity x4 X →
-    {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊎
-      {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]}
-    ⊆@{gmultiset A}
-      {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎
-      {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ X.
+    {[+ x1; x2; x3; x4; x4 +]} ⊎ {[+ x1; x2; x3; x4; x4 +]}
+    ⊆@{gmultiset A} {[+ x1; x1; x2; x3 +]} ⊎ {[+ x1; x1; x2; x3 +]} ⊎ X.
   Proof. multiset_solver. Qed.
   Lemma test_big_4 x1 x2 x3 x4 x5 x6 x7 x8 x9 :
-    {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊎
-      {[ x5 ]} ⊎ {[ x6 ]} ⊎ {[ x7 ]} ⊎ {[ x8 ]} ⊎ {[ x8 ]} ⊎ {[ x9 ]}
+    {[+ x1; x2; x3; x4; x4 +]} ⊎ {[+ x5; x6; x7; x8; x8; x9 +]}
     ⊆@{gmultiset A}
-      {[ x1 ]} ⊎ {[ x1 ]} ⊎ {[ x2 ]} ⊎ {[ x3 ]} ⊎ {[ x4 ]} ⊎ {[ x4 ]} ⊎
-      {[ x5 ]} ⊎ {[ x5 ]} ⊎ {[ x6 ]} ⊎ {[ x7 ]} ⊎ {[ x9 ]} ⊎ {[ x8 ]} ⊎ {[ x8 ]}.
+      {[+ 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).
+    P x ∧ (∀ y, y ∈ X → P y) ↔ (∀ y, y ∈ {[+ x +]} ⊎ X → P y).
   Proof. multiset_solver. Qed.
 End test.
diff --git a/theories/base.v b/theories/base.v
index af97a3f70a0af2bee5f0cfb72525ac8e58b51b72..be247b96e616d2a84676b9cecd9ad01c61899eb7 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -854,14 +854,6 @@ Definition union_list `{Empty A} `{Union A} : list A → A := fold_right (∪) 
 Global Arguments union_list _ _ _ !_ / : assert.
 Notation "⋃ l" := (union_list l) (at level 20, format "⋃  l") : stdpp_scope.
 
-Class DisjUnion A := disj_union: A → A → A.
-Global Hint Mode DisjUnion ! : typeclass_instances.
-Instance: Params (@disj_union) 2 := {}.
-Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
-Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
-Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
-Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
-
 Class Intersection A := intersection: A → A → A.
 Global Hint Mode Intersection ! : typeclass_instances.
 Instance: Params (@intersection) 2 := {}.
@@ -926,12 +918,37 @@ Notation "X ⊆ Y ⊂ Z" := (X ⊆ Y ∧ Y ⊂ Z) (at level 70, Y at next level)
 Notation "X ⊂ Y ⊆ Z" := (X ⊂ Y ∧ Y ⊆ Z) (at level 70, Y at next level) : stdpp_scope.
 Notation "X ⊂ Y ⊂ Z" := (X ⊂ Y ∧ Y ⊂ Z) (at level 70, Y at next level) : stdpp_scope.
 
+(** We define type classes for multisets: disjoint union [⊎] and the multiset
+singleton [{[+ _ +]}]. Multiset literals [{[+ x1; ..; xn +]}] are defined in
+terms of iterated disjoint union [{[+ x1 +]} ⊎ .. ⊎ {[+ xn +]}], and are thus
+different from set literals [{[ x1; ..; xn ]}], which use [∪].
+
+Note that in principle we could reuse the set singleton [{[ _ ]}] for multisets,
+and define [{[+ x1; ..; xn +]}] as [{[ x1 ]} ⊎ .. ⊎ {[ xn ]}]. However, this
+would risk accidentally using [{[ x1; ..; xn ]}] for multisets (leading to
+unexpected results) and lead to ambigious pretty printing for [{[+ x +]}]. *)
+Class DisjUnion A := disj_union: A → A → A.
+Global Hint Mode DisjUnion ! : typeclass_instances.
+Instance: Params (@disj_union) 2 := {}.
+Infix "⊎" := disj_union (at level 50, left associativity) : stdpp_scope.
+Notation "(⊎)" := disj_union (only parsing) : stdpp_scope.
+Notation "( x ⊎.)" := (disj_union x) (only parsing) : stdpp_scope.
+Notation "(.⊎ x )" := (λ y, disj_union y x) (only parsing) : stdpp_scope.
+
+Class SingletonMS A B := singletonMS: A → B.
+Global Hint Mode SingletonMS - ! : typeclass_instances.
+Instance: Params (@singletonMS) 3 := {}.
+Notation "{[+ x +]}" := (singletonMS x) (at level 1) : stdpp_scope.
+Notation "{[+ x ; y ; .. ; z +]}" :=
+  (disj_union .. (disj_union (singletonMS x) (singletonMS y)) .. (singletonMS z))
+  (at level 1) : stdpp_scope.
+
 Definition option_to_set `{Singleton A C, Empty C} (mx : option A) : C :=
   match mx with None => ∅ | Some x => {[ x ]} end.
 Fixpoint list_to_set `{Singleton A C, Empty C, Union C} (l : list A) : C :=
   match l with [] => ∅ | x :: l => {[ x ]} ∪ list_to_set l end.
-Fixpoint list_to_set_disj `{Singleton A C, Empty C, DisjUnion C} (l : list A) : C :=
-  match l with [] => ∅ | x :: l => {[ x ]} ⊎ list_to_set_disj l end.
+Fixpoint list_to_set_disj `{SingletonMS A C, Empty C, DisjUnion C} (l : list A) : C :=
+  match l with [] => ∅ | x :: l => {[+ x +]} ⊎ list_to_set_disj l end.
 
 (** The class [Lexico A] is used for the lexicographic order on [A]. This order
 is used to create finite maps, finite sets, etc, and is typically different from
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index a6782d0efbfafb590d3fcaaccec30f105cf7ef82..c07aa6c3e93ed6ee150d65a12d723e047b5d00fd 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -32,7 +32,7 @@ Section definitions.
   Global Instance gmultiset_size : Size (gmultiset A) := length ∘ elements.
 
   Global Instance gmultiset_empty : Empty (gmultiset A) := GMultiSet ∅.
-  Global Instance gmultiset_singleton : Singleton A (gmultiset A) := λ x,
+  Global Instance gmultiset_singleton : SingletonMS A (gmultiset A) := λ x,
     GMultiSet {[ x := 0 ]}.
   Global Instance gmultiset_union : Union (gmultiset A) := λ X Y,
     let (X) := X in let (Y) := Y in
@@ -78,12 +78,12 @@ Section basic_lemmas.
   (* Multiplicity *)
   Lemma multiplicity_empty x : multiplicity x ∅ = 0.
   Proof. done. Qed.
-  Lemma multiplicity_singleton x : multiplicity x {[ x ]} = 1.
+  Lemma multiplicity_singleton x : multiplicity x {[+ x +]} = 1.
   Proof. unfold multiplicity; simpl. by rewrite lookup_singleton. Qed.
-  Lemma multiplicity_singleton_ne x y : x ≠ y → multiplicity x {[ y ]} = 0.
+  Lemma multiplicity_singleton_ne x y : x ≠ y → multiplicity x {[+ y +]} = 0.
   Proof. intros. unfold multiplicity; simpl. by rewrite lookup_singleton_ne. Qed.
   Lemma multiplicity_singleton' x y :
-    multiplicity x {[ y ]} = if decide (x = y) then 1 else 0.
+    multiplicity x {[+ y +]} = if decide (x = y) then 1 else 0.
   Proof.
     destruct (decide _) as [->|].
     - by rewrite multiplicity_singleton.
@@ -118,21 +118,22 @@ Section basic_lemmas.
   (* Set *)
   Lemma elem_of_multiplicity x X : x ∈ X ↔ 0 < multiplicity x X.
   Proof. done. Qed.
-
-  Global Instance gmultiset_simple_set : SemiSet A (gmultiset A).
+  Lemma gmultiset_elem_of_empty x : x ∈@{gmultiset A} ∅ ↔ False.
+  Proof. rewrite elem_of_multiplicity, multiplicity_empty. lia. Qed.
+  Lemma gmultiset_elem_of_singleton x y : x ∈@{gmultiset A} {[+ y +]} ↔ x = y.
   Proof.
-    split.
-    - intros x. rewrite elem_of_multiplicity, multiplicity_empty. lia.
-    - intros x y.
-      rewrite elem_of_multiplicity, multiplicity_singleton'.
-      destruct (decide (x = y)); intuition lia.
-    - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. lia.
+    rewrite elem_of_multiplicity, multiplicity_singleton'.
+    case_decide; naive_solver lia.
   Qed.
-  Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
-  Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
-
+  Lemma gmultiset_elem_of_union X Y x : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y.
+  Proof. rewrite !elem_of_multiplicity, multiplicity_union. lia. Qed.
   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.
+  Lemma gmultiset_elem_of_intersection X Y x : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y.
+  Proof. rewrite !elem_of_multiplicity, multiplicity_intersection. lia. Qed.
+
+  Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
+  Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
 End basic_lemmas.
 
 (** * A solver for multisets *)
@@ -189,7 +190,7 @@ Section multiset_unfold.
   Global Instance multiset_unfold_empty x : MultisetUnfold x ∅ 0.
   Proof. constructor. by rewrite multiplicity_empty. Qed.
   Global Instance multiset_unfold_singleton x y :
-    MultisetUnfold x {[ x ]} 1.
+    MultisetUnfold x {[+ x +]} 1.
   Proof. constructor. by rewrite multiplicity_singleton. Qed.
   Global Instance multiset_unfold_union x X Y n m :
     MultisetUnfold x X n → MultisetUnfold x Y m →
@@ -238,6 +239,20 @@ Section multiset_unfold.
   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_empty x :
+    SetUnfoldElemOf x (∅ : gmultiset A) False.
+  Proof. constructor. apply gmultiset_elem_of_empty. Qed.
+  Global Instance set_unfold_gmultiset_singleton x y :
+    SetUnfoldElemOf x ({[+ y +]} : gmultiset A) (x = y).
+  Proof. constructor; apply gmultiset_elem_of_singleton. Qed.
+  Global Instance set_unfold_gmultiset_union x X Y P Q :
+    SetUnfoldElemOf x X P → SetUnfoldElemOf x Y Q →
+    SetUnfoldElemOf x (X ∪ Y) (P ∨ Q).
+  Proof.
+    intros ??; constructor. by rewrite gmultiset_elem_of_union,
+      (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
+  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).
@@ -245,6 +260,13 @@ Section multiset_unfold.
     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.
+  Global Instance set_unfold_gmultiset_intersection 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_intersection.
+    by rewrite (set_unfold_elem_of x X P), (set_unfold_elem_of x Y Q).
+  Qed.
 End multiset_unfold.
 
 (** Step 3: instantiate hypotheses *)
@@ -254,7 +276,7 @@ Ltac multiset_instantiate :=
      let e := fresh in evar (e:A);
      let e' := eval unfold e in e in clear e;
      lazymatch constr:(P e') with
-     | context [ {[ ?y ]} ] => unify y e'; learn_hyp (H y)
+     | context [ {[+ ?y +]} ] => unify y e'; learn_hyp (H y)
      end
   | H : (∀ x : ?A, _), _ : context [multiplicity ?y _] |- _ => learn_hyp (H y)
   | H : (∀ x : ?A, _) |- context [multiplicity ?y _] => learn_hyp (H y)
@@ -262,17 +284,17 @@ Ltac multiset_instantiate :=
 
 (** Step 4: simplify singletons *)
 Local Lemma multiplicity_singleton_forget `{Countable A} x y :
-  ∃ n, multiplicity (A:=A) x {[ y ]} = n ∧ n ≤ 1.
+  ∃ n, multiplicity (A:=A) x {[+ y +]} = n ∧ n ≤ 1.
 Proof. rewrite multiplicity_singleton'. case_decide; eauto with lia. Qed.
 
 Ltac multiset_simplify_singletons :=
   repeat match goal with
-  | H : context [multiplicity ?x {[ ?y ]}] |- _ =>
+  | H : context [multiplicity ?x {[+ ?y +]}] |- _ =>
      first
        [progress rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne in H by done
        |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
        |rewrite multiplicity_singleton' in H; destruct (decide (x = y)); simplify_eq/=]
-  | |- context [multiplicity ?x {[ ?y ]}] =>
+  | |- context [multiplicity ?x {[+ ?y +]}] =>
      first
        [progress rewrite ?multiplicity_singleton, ?multiplicity_singleton_ne by done
        |destruct (multiplicity_singleton_forget x y) as (?&->&?); clear y
@@ -347,15 +369,25 @@ Section more_lemmas.
   Lemma gmultiset_disj_union_union_r X Y Z : (X ∪ Y) ⊎ Z = (X ⊎ Z) ∪ (Y ⊎ Z).
   Proof. multiset_solver. Qed.
 
+  (** Element of operation *)
+  Lemma gmultiset_not_elem_of_empty x : x ∉@{gmultiset A} ∅.
+  Proof. multiset_solver. Qed.
+  Lemma gmultiset_not_elem_of_singleton x y : x ∉@{gmultiset A} {[+ y +]} ↔ x ≠ y.
+  Proof. multiset_solver. Qed.
+  Lemma gmultiset_not_elem_of_union x X Y : x ∉ X ∪ Y ↔ x ∉ X ∧ x ∉ Y.
+  Proof. multiset_solver. Qed.
+  Lemma gmultiset_not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
+  Proof. multiset_solver. Qed.
+
   (** Misc *)
-  Lemma gmultiset_non_empty_singleton x : {[ x ]} ≠@{gmultiset A} ∅.
+  Lemma gmultiset_non_empty_singleton x : {[+ x +]} ≠@{gmultiset A} ∅.
   Proof. multiset_solver. Qed.
 
   (** Conversion from lists *)
   Lemma list_to_set_disj_nil : list_to_set_disj [] =@{gmultiset A} ∅.
   Proof. done. Qed.
   Lemma list_to_set_disj_cons x l :
-    list_to_set_disj (x :: l) =@{gmultiset A} {[ x ]} ⊎ list_to_set_disj l.
+    list_to_set_disj (x :: l) =@{gmultiset A} {[+ x +]} ⊎ list_to_set_disj l.
   Proof. done. Qed.
   Lemma list_to_set_disj_app l1 l2 :
     list_to_set_disj (l1 ++ l2) =@{gmultiset A} list_to_set_disj l1 ⊎ list_to_set_disj l2.
@@ -381,7 +413,7 @@ Section more_lemmas.
     split; intros HX; [by apply gmultiset_elements_empty_inv|].
     by rewrite HX, gmultiset_elements_empty.
   Qed.
-  Lemma gmultiset_elements_singleton x : elements ({[ x ]} : gmultiset A) = [ x ].
+  Lemma gmultiset_elements_singleton x : elements ({[+ x +]} : gmultiset A) = [ x ].
   Proof.
     unfold elements, gmultiset_elements; simpl. by rewrite map_to_list_singleton.
   Qed.
@@ -427,7 +459,7 @@ Section more_lemmas.
     set_fold f b (∅ : gmultiset A) = b.
   Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_empty. Qed.
   Lemma gmultiset_set_fold_singleton {B} (f : A → B → B) (b : B) (a : A) :
-    set_fold f b ({[a]} : gmultiset A) = f a b.
+    set_fold f b ({[+ a +]} : gmultiset A) = f a b.
   Proof. by unfold set_fold; simpl; rewrite gmultiset_elements_singleton. Qed.
   Lemma gmultiset_set_fold_disj_union (f : A → A → A) (b : A) X Y :
     Comm (=) f →
@@ -468,7 +500,7 @@ Section more_lemmas.
     contradict Hsz. rewrite HX, gmultiset_size_empty; lia.
   Qed.
 
-  Lemma gmultiset_size_singleton x : size ({[ x ]} : gmultiset A) = 1.
+  Lemma gmultiset_size_singleton x : size ({[+ x +]} : gmultiset A) = 1.
   Proof.
     unfold size, gmultiset_size; simpl. by rewrite gmultiset_elements_singleton.
   Qed.
@@ -531,7 +563,7 @@ Section more_lemmas.
   Lemma gmultiset_union_subset_r X Y : X ≠ ∅ → Y ⊂ X ⊎ Y.
   Proof. multiset_solver. Qed.
 
-  Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[ x ]} ⊆ X.
+  Lemma gmultiset_elem_of_singleton_subseteq x X : x ∈ X ↔ {[+ x +]} ⊆ X.
   Proof. multiset_solver. Qed.
 
   Lemma gmultiset_elem_of_subseteq X1 X2 x : x ∈ X1 → X1 ⊆ X2 → x ∈ X2.
@@ -539,7 +571,8 @@ Section more_lemmas.
 
   Lemma gmultiset_disj_union_difference X Y : X ⊆ Y → Y = X ⊎ Y ∖ X.
   Proof. multiset_solver. Qed.
-  Lemma gmultiset_disj_union_difference' x Y : x ∈ Y → Y = {[ x ]} ⊎ Y ∖ {[ x ]}.
+  Lemma gmultiset_disj_union_difference' x Y :
+    x ∈ Y → Y = {[+ x +]} ⊎ Y ∖ {[+ x +]}.
   Proof. multiset_solver. Qed.
 
   Lemma gmultiset_size_difference X Y : Y ⊆ X → size (X ∖ Y) = size X - size Y.
@@ -585,7 +618,7 @@ Section more_lemmas.
   Qed.
 
   Lemma gmultiset_ind (P : gmultiset A → Prop) :
-    P ∅ → (∀ x X, P X → P ({[ x ]} ⊎ X)) → ∀ X, P X.
+    P ∅ → (∀ x X, P X → P ({[+ x +]} ⊎ X)) → ∀ X, P X.
   Proof.
     intros Hemp Hinsert X. induction (gmultiset_wf X) as [X _ IH].
     destruct (gmultiset_choose_or_empty X) as [[x Hx]| ->]; auto.