diff --git a/theories/base.v b/theories/base.v
index d4005a4dfaa24eb400f8eda6b77c7e8b54a8aa0d..801af5bf93beb6768dcafe9b5d3ed725a9934a31 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -856,6 +856,9 @@ Notation "(∉)" := (λ x X, x ∉ X) (only parsing) : stdpp_scope.
 Notation "( x ∉)" := (λ X, x ∉ X) (only parsing) : stdpp_scope.
 Notation "(∉ X )" := (λ x, x ∉ X) (only parsing) : stdpp_scope.
 
+Infix "∈@{ B }" := (@elem_of _ B _) (at level 70, only parsing) : stdpp_scope.
+Notation "(∈@{ B } )" := (@elem_of _ B _) (only parsing) : stdpp_scope.
+
 Class Disjoint A := disjoint : A → A → Prop.
  Hint Mode Disjoint ! : typeclass_instances.
 Instance: Params (@disjoint) 2.
diff --git a/theories/bset.v b/theories/bset.v
index 1c17ee660e15cf56fe6600088f18726395718c7c..f0b7a05037b75f08b6fc4462440d57c814b681eb 100644
--- a/theories/bset.v
+++ b/theories/bset.v
@@ -29,7 +29,7 @@ Proof.
   - intros X Y x; unfold elem_of, bset_elem_of; simpl. 
     destruct (bset_car X x), (bset_car Y x); simpl; tauto.
 Qed.
-Instance bset_elem_of_dec {A} : RelDecision (@elem_of _ (bset A) _).
+Instance bset_elem_of_dec {A} : RelDecision (∈@{bset A}).
 Proof. refine (λ x X, cast_if (decide (bset_car X x))); done. Defined.
 
 Typeclasses Opaque bset_elem_of.
diff --git a/theories/coPset.v b/theories/coPset.v
index 5c027492dd717ed2189629bfc66ffe4cbbfb5332..77b0d2b29c6409efc3c821a38514a4017a546bf1 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -190,7 +190,7 @@ Proof.
   intros p; apply eq_bool_prop_intro, (HXY p).
 Qed.
 
-Instance coPset_elem_of_dec : RelDecision (@elem_of _ coPset _).
+Instance coPset_elem_of_dec : RelDecision (∈@{coPset}).
 Proof. solve_decision. Defined.
 Instance coPset_equiv_dec : RelDecision (≡@{coPset}).
 Proof. refine (λ X Y, cast_if (decide (X = Y))); abstract (by fold_leibniz). Defined.
diff --git a/theories/collections.v b/theories/collections.v
index 93f3d435042f8043b538e7ee442250e192aa15ea..cc4b9cc76a71084d68f7d808edeca8d579cf8401 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -28,8 +28,7 @@ Section setoids_simple.
   Qed.
   Global Instance singleton_proper : Proper ((=) ==> (≡@{C})) singleton.
   Proof. apply _. Qed.
-  Global Instance elem_of_proper :
-    Proper ((=) ==> (≡) ==> iff) (@elem_of A C _) | 5.
+  Global Instance elem_of_proper : Proper ((=) ==> (≡) ==> iff) (∈@{C}) | 5.
   Proof. by intros x ? <- X Y. Qed.
   Global Instance disjoint_proper: Proper ((≡) ==> (≡) ==> iff) (@disjoint C _).
   Proof.
@@ -695,7 +694,7 @@ Section collection.
   End leibniz.
 
   Section dec.
-    Context `{!RelDecision (@elem_of A C _)}.
+    Context `{!RelDecision (∈@{C})}.
     Lemma not_elem_of_intersection x X Y : x ∉ X ∩ Y ↔ x ∉ X ∨ x ∉ Y.
     Proof. rewrite elem_of_intersection. destruct (decide (x ∈ X)); tauto. Qed.
     Lemma not_elem_of_difference x X Y : x ∉ X ∖ Y ↔ x ∉ X ∨ x ∈ Y.
diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index c2e6487e7459e22a22cbd8e0aebca231415b4e14..0d9f16e86cba791ae3737b408bbd907c94d5c5cf 100644
--- a/theories/fin_collections.v
+++ b/theories/fin_collections.v
@@ -23,7 +23,7 @@ Implicit Types X Y : C.
 Lemma fin_collection_finite X : set_finite X.
 Proof. by exists (elements X); intros; rewrite elem_of_elements. Qed.
 
-Instance elem_of_dec_slow : RelDecision (@elem_of A C _) | 100.
+Instance elem_of_dec_slow : RelDecision (∈@{C}) | 100.
 Proof.
   refine (λ x X, cast_if (decide_rel (∈) x (elements X)));
     by rewrite <-(elem_of_elements _).
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index 4cc990e24da30c6b7ccd0978bdc8dd8ca3bf1232..ab6583c1206d9badfbc099f652840d83899bf7fa 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -98,7 +98,7 @@ Proof.
       by split; auto with lia.
   - intros X Y x. rewrite !elem_of_multiplicity, multiplicity_union. omega.
 Qed.
-Global Instance gmultiset_elem_of_dec : RelDecision (@elem_of _ (gmultiset A) _).
+Global Instance gmultiset_elem_of_dec : RelDecision (∈@{gmultiset A}).
 Proof. refine (λ x X, cast_if (decide (0 < multiplicity x X))); done. Defined.
 
 (* Algebraic laws *)
diff --git a/theories/infinite.v b/theories/infinite.v
index 7b5c08f8c551b3ca75a68b92521958f0ee1846d1..81863ebc800f2a5214829dded22bab57e7b204f1 100644
--- a/theories/infinite.v
+++ b/theories/infinite.v
@@ -26,7 +26,7 @@ Qed.
 
 (** * Fresh elements *)
 Section Fresh.
-  Context `{FinCollection A C, Infinite A, !RelDecision (@elem_of A C _)}.
+  Context `{FinCollection A C, Infinite A, !RelDecision (∈@{C})}.
 
   Definition fresh_generic_body (s : C) (rec : ∀ s', s' ⊂ s → nat → A) (n : nat) : A :=
     let cand := inject n in
diff --git a/theories/list.v b/theories/list.v
index e5ac38d913aa57367db82de1d916805f41f1d283..d5df07c7e62c6235fd24f1fa78c33655c8858ac1 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -311,7 +311,7 @@ Instance list_subseteq {A} : SubsetEq (list A) := λ l1 l2, ∀ x, x ∈ l1 →
 
 Section list_set.
   Context `{dec : EqDecision A}.
-  Global Instance elem_of_list_dec : RelDecision (@elem_of A (list A) _).
+  Global Instance elem_of_list_dec : RelDecision (∈@{list A}).
   Proof.
    refine (
     fix go x l :=
diff --git a/theories/mapset.v b/theories/mapset.v
index b814d68f0b9bafbad5c869d572f810220d538236..fa5e02e593bdcc0cb70513c4814342cc486d1a61 100644
--- a/theories/mapset.v
+++ b/theories/mapset.v
@@ -78,7 +78,7 @@ Section deciders.
   Defined.
   Global Instance mapset_equiv_dec : RelDecision (≡@{mapset M}) | 1.
   Proof. refine (λ X1 X2, cast_if (decide (X1 = X2))); abstract (by fold_leibniz). Defined.
-  Global Instance mapset_elem_of_dec : RelDecision (@elem_of _ (mapset M) _) | 1.
+  Global Instance mapset_elem_of_dec : RelDecision (∈@{mapset M}) | 1.
   Proof. refine (λ x X, cast_if (decide (mapset_car X !! x = Some ()))); done. Defined.
   Global Instance mapset_disjoint_dec : RelDecision (@disjoint (mapset M) _).
   Proof.