diff --git a/algebra/dec_agree.v b/algebra/dec_agree.v
index 068ec54b1907a4413779aded2f9c2ba588ad52cf..2a71934e9316433d0e85225981237719b2d141ba 100644
--- a/algebra/dec_agree.v
+++ b/algebra/dec_agree.v
@@ -14,7 +14,7 @@ Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
   match x with DecAgree a => Some a | _ => None end.
 
 Section dec_agree.
-Context {A : Type} `{∀ x y : A, Decision (x = y)}.
+Context `{EqDecision A}.
 
 Instance dec_agree_valid : Valid (dec_agree A) := λ x,
   if x is DecAgree _ then True else False.
diff --git a/algebra/iprod.v b/algebra/iprod.v
index 181e5d80de9b0a417e2818a7ae79cb87e67c8289..2e8d1f23974e162faaeb4f08e8c7038793859398 100644
--- a/algebra/iprod.v
+++ b/algebra/iprod.v
@@ -39,7 +39,7 @@ Section iprod_cofe.
   Canonical Structure iprodC : cofeT := CofeT (iprod B) iprod_cofe_mixin.
 
   (** Properties of iprod_insert. *)
-  Context `{∀ x x' : A, Decision (x = x')}.
+  Context `{EqDecision A}.
 
   Global Instance iprod_insert_ne n x :
     Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index 8f6bac10b0424eb691f7303a195af81432b429a2..6a0f8af99a5fceb30c47b4791cf09fa6725264f2 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -22,7 +22,7 @@ Bind Scope binder_scope with binder.
 Definition cons_binder (mx : binder) (X : list string) : list string :=
   match mx with BAnon => X | BNamed x => x :: X end.
 Infix ":b:" := cons_binder (at level 60, right associativity).
-Instance binder_dec_eq (x1 x2 : binder) : Decision (x1 = x2).
+Instance binder_eq_dec_eq : EqDecision binder.
 Proof. solve_decision. Defined.
 
 Instance set_unfold_cons_binder x mx X P :
@@ -125,17 +125,17 @@ Qed.
 Instance of_val_inj : Inj (=) (=) of_val.
 Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-Instance base_lit_dec_eq (l1 l2 : base_lit) : Decision (l1 = l2).
+Instance base_lit_eq_dec : EqDecision base_lit.
 Proof. solve_decision. Defined.
-Instance un_op_dec_eq (op1 op2 : un_op) : Decision (op1 = op2).
+Instance un_op_eq_dec : EqDecision un_op.
 Proof. solve_decision. Defined.
-Instance bin_op_dec_eq (op1 op2 : bin_op) : Decision (op1 = op2).
+Instance bin_op_eq_dec : EqDecision bin_op.
 Proof. solve_decision. Defined.
-Instance expr_dec_eq (e1 e2 : expr) : Decision (e1 = e2).
+Instance expr_eq_dec : EqDecision expr.
 Proof. solve_decision. Defined.
-Instance val_dec_eq (v1 v2 : val) : Decision (v1 = v2).
+Instance val_eq_dec : EqDecision val.
 Proof.
- refine (cast_if (decide (of_val v1 = of_val v2))); abstract naive_solver.
+ refine (λ v v', cast_if (decide (of_val v = of_val v'))); abstract naive_solver.
 Defined.
 
 Instance expr_inhabited : Inhabited expr := populate (Lit LitUnit).
diff --git a/prelude/base.v b/prelude/base.v
index b7b02e23078068d7a642ad2b1254317f1358c6d9..8f01258a121363b1fab7f29949b8ae6957fb2800 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -100,6 +100,7 @@ on a type [A] we write [`{∀ x y : A, Decision (x = y)}] and use it by writing
 [decide (x = y)]. *)
 Class Decision (P : Prop) := decide : {P} + {¬P}.
 Arguments decide _ {_}.
+Notation EqDecision A := (∀ x y : A, Decision (x = y)).
 
 (** ** Inhabited types *)
 (** This type class collects types that are inhabited. *)
@@ -918,9 +919,8 @@ Inductive NoDup {A} : list A → Prop :=
 
 (** Decidability of equality of the carrier set is admissible, but we add it
 anyway so as to avoid cycles in type class search. *)
-Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C,
-    Union C, Intersection C, Difference C,
-    Elements A C, ∀ x y : A, Decision (x = y)} : Prop := {
+Class FinCollection A C `{ElemOf A C, Empty C, Singleton A C, Union C,
+    Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
   fin_collection :>> Collection A C;
   elem_of_elements X x : x ∈ elements X ↔ x ∈ X;
   NoDup_elements X : NoDup (elements X)
diff --git a/prelude/bset.v b/prelude/bset.v
index f0da19b3536a1ba684fb78914cfe10761eef99c5..92a6f22624250d92ceac57bae627859174e95759 100644
--- a/prelude/bset.v
+++ b/prelude/bset.v
@@ -8,8 +8,8 @@ Arguments mkBSet {_} _.
 Arguments bset_car {_} _ _.
 Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
 Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
-Instance bset_singleton {A} `{∀ x y : A, Decision (x = y)} :
-  Singleton A (bset A) := λ x, mkBSet (λ y, bool_decide (y = x)).
+Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x,
+  mkBSet (λ y, bool_decide (y = x)).
 Instance bset_elem_of {A} : ElemOf A (bset A) := λ x X, bset_car X x.
 Instance bset_union {A} : Union (bset A) := λ X1 X2,
   mkBSet (λ x, bset_car X1 x || bset_car X2 x).
@@ -17,8 +17,7 @@ Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2,
   mkBSet (λ x, bset_car X1 x && bset_car X2 x).
 Instance bset_difference {A} : Difference (bset A) := λ X1 X2,
   mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)).
-Instance bset_collection {A} `{∀ x y : A, Decision (x = y)} :
-  Collection A (bset A).
+Instance bset_collection `{EqDecision A} : Collection A (bset A).
 Proof.
   split; [split| |].
   - by intros x ?.
diff --git a/prelude/coPset.v b/prelude/coPset.v
index 85aec1c9cb567e4cecc8ea2c2d95bc762e69fe3c..821504c5403d6e67206919973bfc16285697ec52 100644
--- a/prelude/coPset.v
+++ b/prelude/coPset.v
@@ -19,7 +19,7 @@ Local Open Scope positive_scope.
 Inductive coPset_raw :=
   | coPLeaf : bool → coPset_raw
   | coPNode : bool → coPset_raw → coPset_raw → coPset_raw.
-Instance coPset_raw_eq_dec (t1 t2 : coPset_raw) : Decision (t1 = t2).
+Instance coPset_raw_eq_dec : EqDecision coPset_raw.
 Proof. solve_decision. Defined.
 
 Fixpoint coPset_wf (t : coPset_raw) : bool :=
diff --git a/prelude/countable.v b/prelude/countable.v
index a2aad6cc5181a3cab0679c9288d8e56d8a88cba4..ef4b44b9a11b3acab1d53940fa63026f62193911 100644
--- a/prelude/countable.v
+++ b/prelude/countable.v
@@ -3,7 +3,7 @@
 From iris.prelude Require Export list.
 Local Open Scope positive.
 
-Class Countable A `{∀ x y : A, Decision (x = y)} := {
+Class Countable A `{EqDecision A} := {
   encode : A → positive;
   decode : positive → option A;
   decode_encode x : decode (encode x) = Some x
@@ -70,7 +70,7 @@ Section choice.
   Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA.
 End choice.
 
-Lemma surj_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
+Lemma surj_cancel `{Countable A} `{EqDecision B}
   (f : A → B) `{!Surj (=) f} : { g : B → A & Cancel (=) f g }.
 Proof.
   exists (λ y, choose (λ x, f x = y) (surj f y)).
@@ -80,7 +80,7 @@ Qed.
 (** * Instances *)
 (** ** Injection *)
 Section injective_countable.
-  Context `{Countable A, ∀ x y : B, Decision (x = y)}.
+  Context `{Countable A, EqDecision B}.
   Context (f : B → A) (g : A → option B) (fg : ∀ x, g (f x) = Some x).
 
   Program Instance injective_countable : Countable B :=
diff --git a/prelude/decidable.v b/prelude/decidable.v
index 7b6431a6f371b738060c9d957440c276e4c44270..9c7ec3ab4693d8d60958fa883ccec354c67eab19 100644
--- a/prelude/decidable.v
+++ b/prelude/decidable.v
@@ -164,15 +164,13 @@ Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
   Decision (P ↔ Q) := and_dec _ _.
 
 (** Instances of [Decision] for common data types. *)
-Instance bool_eq_dec (x y : bool) : Decision (x = y).
+Instance bool_eq_dec : EqDecision bool.
 Proof. solve_decision. Defined.
-Instance unit_eq_dec (x y : unit) : Decision (x = y).
+Instance unit_eq_dec : EqDecision unit.
 Proof. solve_decision. Defined.
-Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
-  `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
+Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
 Proof. solve_decision. Defined.
-Instance sum_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
-  `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
+Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
 Proof. solve_decision. Defined.
 
 Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
@@ -181,9 +179,11 @@ Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
   | (x,y) => P_dec x y
   end.
 
-Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
-  `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
-Proof. refine (cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial. Defined.
+Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
+  EqDecision (sig P).
+Proof.
+ refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
+Defined.
 
 (** Some laws for decidable propositions *)
 Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
diff --git a/prelude/fin_map_dom.v b/prelude/fin_map_dom.v
index afb29ae11ec685fe7e421e7881829156de69dfdb..3a657eb433436f942547b35dabba6f4279bb38c4 100644
--- a/prelude/fin_map_dom.v
+++ b/prelude/fin_map_dom.v
@@ -7,7 +7,7 @@ From iris.prelude Require Export collections fin_maps.
 
 Class FinMapDom K M D `{FMap M,
     ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
-    OMap M, Merge M, ∀ A, FinMapToList K A (M A), ∀ i j : K, Decision (i = j),
+    OMap M, Merge M, ∀ A, FinMapToList K A (M A), EqDecision K,
     ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D,
     Union D, Intersection D, Difference D} := {
   finmap_dom_map :>> FinMap K M;
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 5f4b4bcae225abf461877c3ff773ae1431d04689..2f75f6b98a9c77aff98ac73f6e21084d4a5ad4e8 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -27,7 +27,7 @@ Class FinMapToList K A M := map_to_list: M → list (K * A).
 
 Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
     PartialAlter K A (M A), OMap M, Merge M, ∀ A, FinMapToList K A (M A),
-    ∀ i j : K, Decision (i = j)} := {
+    EqDecision K} := {
   map_eq {A} (m1 m2 : M A) : (∀ i, m1 !! i = m2 !! i) → m1 = m2;
   lookup_empty {A} i : (∅ : M A) !! i = None;
   lookup_partial_alter {A} f (m : M A) i :
diff --git a/prelude/finite.v b/prelude/finite.v
index 06a7db2695bab832b36229eec980cb7c598636cc..880df63b2073b5ef7d7ed2713ca37da7fe59ed9a 100644
--- a/prelude/finite.v
+++ b/prelude/finite.v
@@ -2,7 +2,7 @@
 (* This file is distributed under the terms of the BSD license. *)
 From iris.prelude Require Export countable vector.
 
-Class Finite A `{∀ x y : A, Decision (x = y)} := {
+Class Finite A `{EqDecision A} := {
   enum : list A;
   NoDup_enum : NoDup enum;
   elem_of_enum x : x ∈ enum
@@ -189,7 +189,7 @@ End forall_exists.
 
 (** Instances *)
 Section enc_finite.
-  Context `{∀ x y : A, Decision (x = y)}.
+  Context `{EqDecision A}.
   Context (to_nat : A → nat) (of_nat : nat → A) (c : nat).
   Context (of_to_nat : ∀ x, of_nat (to_nat x) = x).
   Context (to_nat_c : ∀ x, to_nat x < c).
@@ -212,7 +212,7 @@ Section enc_finite.
 End enc_finite.
 
 Section bijective_finite.
-  Context `{Finite A, ∀ x y : B, Decision (x = y)} (f : A → B) (g : B → A).
+  Context `{Finite A, EqDecision B} (f : A → B) (g : B → A).
   Context `{!Inj (=) (=) f, !Cancel (=) f g}.
 
   Program Instance bijective_finite: Finite B := {| enum := f <$> enum A |}.
diff --git a/prelude/functions.v b/prelude/functions.v
index 935d1b448b9dcbd9c1b62f790e57004b341c2e35..113ce19ec54634321b599a881ad8b084f9540088 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -1,7 +1,7 @@
 From iris.prelude Require Export base tactics.
 
 Section definitions.
-  Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
+  Context {A T : Type} `{EqDecision A}.
   Global Instance fn_insert : Insert A T (A → T) :=
     λ a t f b, if decide (a = b) then t else f b.
   Global Instance fn_alter : Alter A T (A → T) :=
@@ -12,7 +12,7 @@ End definitions.
    of equality of functions. *)
 
 Section functions.
-  Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
+  Context {A T : Type} `{!EqDecision A}.
 
   Lemma fn_lookup_insert (f : A → T) a t : <[a:=t]>f a = t.
   Proof. unfold insert, fn_insert. by destruct (decide (a = a)). Qed.
diff --git a/prelude/gmap.v b/prelude/gmap.v
index e87f1434ea69bbd17ad1c2c75390bb0af1fe2447..dfb504396590fe514ae7d64a5d9a0303ad236745 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -22,10 +22,9 @@ Proof.
   split; [by intros ->|intros]. destruct m1, m2; simplify_eq/=.
   f_equal; apply proof_irrel.
 Qed.
-Instance gmap_eq_eq `{Countable K} `{∀ x y : A, Decision (x = y)}
-  (m1 m2 : gmap K A) : Decision (m1 = m2).
+Instance gmap_eq_eq `{Countable K, EqDecision A} : EqDecision (gmap K A).
 Proof.
- refine (cast_if (decide (gmap_car m1 = gmap_car m2)));
+ refine (λ m1 m2, cast_if (decide (gmap_car m1 = gmap_car m2)));
   abstract (by rewrite gmap_eq).
 Defined.
 
diff --git a/prelude/hashset.v b/prelude/hashset.v
index 4c229b5e8f6f78162b08b0a9eb8c1cc6dfc4b293..dea9c7c02db921c691d363e8e51cc0bd7738baa3 100644
--- a/prelude/hashset.v
+++ b/prelude/hashset.v
@@ -15,7 +15,7 @@ Arguments Hashset {_ _} _ _.
 Arguments hashset_car {_ _} _.
 
 Section hashset.
-Context `{∀ x y : A, Decision (x = y)} (hash : A → Z).
+Context `{EqDecision A} (hash : A → Z).
 
 Instance hashset_elem_of: ElemOf A (hashset hash) := λ x m, ∃ l,
   hashset_car m !! hash x = Some l ∧ x ∈ l.
@@ -137,7 +137,7 @@ Hint Extern 1 (Elements _ (hashset _)) =>
   eapply @hashset_elems : typeclass_instances.
 
 Section remove_duplicates.
-Context `{∀ x y : A, Decision (x = y)} (hash : A → Z).
+Context `{EqDecision A} (hash : A → Z).
 
 Definition remove_dups_fast (l : list A) : list A :=
   match l with
diff --git a/prelude/list.v b/prelude/list.v
index e349d2fd441acdc86234de1b6ca3e7999c68aa4c..c5f4ee34cfd3ff8cca664846377079fa29315ab2 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -245,7 +245,8 @@ Hint Extern 0 (_ `prefix_of` _) => reflexivity.
 Hint Extern 0 (_ `suffix_of` _) => reflexivity.
 
 Section prefix_suffix_ops.
-  Context `{∀ x y : A, Decision (x = y)}.
+  Context `{EqDecision A}.
+
   Definition max_prefix_of : list A → list A → list A * list A * list A :=
     fix go l1 l2 :=
     match l1, l2 with
@@ -284,7 +285,7 @@ Infix "`contains`" := contains (at level 70) : C_scope.
 Hint Extern 0 (_ `contains` _) => reflexivity.
 
 Section contains_dec_help.
-  Context {A} {dec : ∀ x y : A, Decision (x = y)}.
+  Context `{EqDecision A}.
   Fixpoint list_remove (x : A) (l : list A) : option (list A) :=
     match l with
     | [] => None
@@ -302,14 +303,13 @@ Inductive Forall3 {A B C} (P : A → B → C → Prop) :
   | Forall3_cons x y z l k k' :
      P x y z → Forall3 P l k k' → Forall3 P (x :: l) (y :: k) (z :: k').
 
-(** Set operations on lists *)
+(** Set operations Decisionon lists *)
 Definition included {A} (l1 l2 : list A) := ∀ x, x ∈ l1 → x ∈ l2.
 Infix "`included`" := included (at level 70) : C_scope.
 
 Section list_set.
-  Context {A} {dec : ∀ x y : A, Decision (x = y)}.
-  Global Instance elem_of_list_dec {dec : ∀ x y : A, Decision (x = y)}
-    (x : A) : ∀ l, Decision (x ∈ l).
+  Context `{dec : EqDecision A}.
+  Global Instance elem_of_list_dec (x : A) : ∀ l, Decision (x ∈ l).
   Proof.
    refine (
     fix go l :=
@@ -415,8 +415,8 @@ Proof.
   - discriminate (H 0).
   - f_equal; [by injection (H 0)|]. apply (IH _ $ λ i, H (S i)).
 Qed.
-Global Instance list_eq_dec {dec : ∀ x y, Decision (x = y)} : ∀ l k,
-  Decision (l = k) := list_eq_dec dec.
+Global Instance list_eq_dec {dec : EqDecision A} : EqDecision (list A) :=
+  list_eq_dec dec.
 Global Instance list_eq_nil_dec l : Decision (l = []).
 Proof. by refine match l with [] => left _ | _ => right _ end. Defined.
 Lemma list_singleton_reflect l :
@@ -695,7 +695,7 @@ Proof.
 Qed.
 
 Section no_dup_dec.
-  Context `{!∀ x y, Decision (x = y)}.
+  Context `{!EqDecision A}.
   Global Instance NoDup_dec: ∀ l, Decision (NoDup l) :=
     fix NoDup_dec l :=
     match l return Decision (NoDup l) with
@@ -724,7 +724,7 @@ End no_dup_dec.
 
 (** ** Set operations on lists *)
 Section list_set.
-  Context {dec : ∀ x y, Decision (x = y)}.
+  Context `{!EqDecision A}.
   Lemma elem_of_list_difference l k x : x ∈ list_difference l k ↔ x ∈ l ∧ x ∉ k.
   Proof.
     split; induction l; simpl; try case_decide;
@@ -1443,7 +1443,7 @@ Proof.
   - intros ?. by eexists [].
   - intros ???[k1->] [k2->]. exists (k2 ++ k1). by rewrite (assoc_L (++)).
 Qed.
-Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
+Global Instance prefix_of_dec `{!EqDecision A} : ∀ l1 l2,
     Decision (l1 `prefix_of` l2) := fix go l1 l2 :=
   match l1, l2 return { l1 `prefix_of` l2 } + { ¬l1 `prefix_of` l2 } with
   | [], _ => left (prefix_of_nil _)
@@ -1460,7 +1460,7 @@ Global Instance prefix_of_dec `{∀ x y, Decision (x = y)} : ∀ l1 l2,
   end.
 
 Section prefix_ops.
-  Context `{∀ x y, Decision (x = y)}.
+  Context `{!EqDecision A}.
   Lemma max_prefix_of_fst l1 l2 :
     l1 = (max_prefix_of l1 l2).2 ++ (max_prefix_of l1 l2).1.1.
   Proof.
@@ -1577,7 +1577,7 @@ Lemma suffix_of_length l1 l2 : l1 `suffix_of` l2 → length l1 ≤ length l2.
 Proof. intros [? ->]. rewrite app_length. lia. Qed.
 Lemma suffix_of_cons_not x l : ¬x :: l `suffix_of` l.
 Proof. intros [??]. discriminate_list. Qed.
-Global Instance suffix_of_dec `{∀ x y, Decision (x = y)} l1 l2 :
+Global Instance suffix_of_dec `{!EqDecision A} l1 l2 :
   Decision (l1 `suffix_of` l2).
 Proof.
   refine (cast_if (decide_rel prefix_of (reverse l1) (reverse l2)));
@@ -1585,7 +1585,7 @@ Proof.
 Defined.
 
 Section max_suffix_of.
-  Context `{∀ x y, Decision (x = y)}.
+  Context `{!EqDecision A}.
 
   Lemma max_suffix_of_fst l1 l2 :
     l1 = (max_suffix_of l1 l2).1.1 ++ (max_suffix_of l1 l2).2.
@@ -1987,7 +1987,7 @@ Proof.
 Qed.
 
 Section contains_dec.
-  Context `{∀ x y, Decision (x = y)}.
+  Context `{!EqDecision A}.
 
   Lemma list_remove_Permutation l1 l2 k1 x :
     l1 ≡ₚ l2 → list_remove x l1 = Some k1 →
@@ -2215,16 +2215,16 @@ Section Forall_Exists.
   Lemma Forall_not_Exists l : Forall (not ∘ P) l → ¬Exists P l.
   Proof. induction 1; inversion_clear 1; contradiction. Qed.
 
-  Lemma Forall_list_difference `{∀ x y : A, Decision (x = y)} l k :
+  Lemma Forall_list_difference `{!EqDecision A} l k :
     Forall P l → Forall P (list_difference l k).
   Proof.
     rewrite !Forall_forall.
     intros ? x; rewrite elem_of_list_difference; naive_solver.
   Qed.
-  Lemma Forall_list_union `{∀ x y : A, Decision (x = y)} l k :
+  Lemma Forall_list_union `{!EqDecision A} l k :
     Forall P l → Forall P k → Forall P (list_union l k).
   Proof. intros. apply Forall_app; auto using Forall_list_difference. Qed.
-  Lemma Forall_list_intersection `{∀ x y : A, Decision (x = y)} l k :
+  Lemma Forall_list_intersection `{!EqDecision A} l k :
     Forall P l → Forall P (list_intersection l k).
   Proof.
     rewrite !Forall_forall.
diff --git a/prelude/listset.v b/prelude/listset.v
index 1d2947de09218472df2128df718c55c19c2b2aeb..7987bf223cae39d5c8fc768a8b72361b3db1fc9d 100644
--- a/prelude/listset.v
+++ b/prelude/listset.v
@@ -37,7 +37,7 @@ Proof.
   abstract (by rewrite listset_empty_alt).
 Defined.
 
-Context `{∀ x y : A, Decision (x = y)}.
+Context `{!EqDecision A}.
 
 Instance listset_intersection: Intersection (listset A) := λ l k,
   let (l') := l in let (k') := k in Listset (list_intersection l' k').
diff --git a/prelude/listset_nodup.v b/prelude/listset_nodup.v
index ab4ac765d5a783edff2d5f335f2fcc1632355a38..25843624ef383e66b0f7b000b3b89b853e58b9ba 100644
--- a/prelude/listset_nodup.v
+++ b/prelude/listset_nodup.v
@@ -13,7 +13,7 @@ Arguments listset_nodup_car {_} _.
 Arguments listset_nodup_prf {_} _.
 
 Section list_collection.
-Context {A : Type} `{∀ x y : A, Decision (x = y)}.
+Context `{EqDecision A}.
 Notation C := (listset_nodup A).
 
 Instance listset_nodup_elem_of: ElemOf A C := λ x l, x ∈ listset_nodup_car l.
diff --git a/prelude/mapset.v b/prelude/mapset.v
index 5a3dd7188e4f8c9f97737f0910996fe2b0bae3a1..20b5b6e6dec8859c715974b8d59651927082f01a 100644
--- a/prelude/mapset.v
+++ b/prelude/mapset.v
@@ -68,11 +68,11 @@ Proof.
 Qed.
 
 Section deciders.
-  Context `{∀ m1 m2 : M unit, Decision (m1 = m2)}.
-  Global Instance mapset_eq_dec (X1 X2 : mapset M) : Decision (X1 = X2) | 1.
+  Context `{EqDecision (M unit)}.
+  Global Instance mapset_eq_dec : EqDecision (mapset M) | 1.
   Proof.
-   refine
-    match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end;
+   refine (λ X1 X2,
+    match X1, X2 with Mapset m1, Mapset m2 => cast_if (decide (m1 = m2)) end);
     abstract congruence.
   Defined.
   Global Instance mapset_equiv_dec (X1 X2 : mapset M) : Decision (X1 ≡ X2) | 1.
diff --git a/prelude/natmap.v b/prelude/natmap.v
index 5845901a62cf9d3fe2fc6b63806409e5c1e86b05..f3491a1c16857f5c6a0adeff75deef8c6a9ef805 100644
--- a/prelude/natmap.v
+++ b/prelude/natmap.v
@@ -36,8 +36,7 @@ Proof.
   split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
   simplify_eq/=; f_equal; apply proof_irrel.
 Qed.
-Global Instance natmap_eq_dec `{∀ x y : A, Decision (x = y)}
-    (m1 m2 : natmap A) : Decision (m1 = m2) :=
+Global Instance natmap_eq_dec `{EqDecision A} : EqDecision (natmap A) := λ m1 m2,
   match decide (natmap_car m1 = natmap_car m2) with
   | left H => left (proj2 (natmap_eq m1 m2) H)
   | right H => right (H ∘ proj1 (natmap_eq m1 m2))
diff --git a/prelude/nmap.v b/prelude/nmap.v
index 11fead13c53c361d4e852924c79a4aae2e08f425..19bc574c71a884fba952ff80408b8e5c60325430 100644
--- a/prelude/nmap.v
+++ b/prelude/nmap.v
@@ -12,13 +12,12 @@ Arguments Nmap_0 {_} _.
 Arguments Nmap_pos {_} _.
 Arguments NMap {_} _ _.
 
-Instance Nmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Nmap A) :
-  Decision (t1 = t2).
+Instance Nmap_eq_dec `{EqDecision A} : EqDecision (Nmap A).
 Proof.
- refine
+ refine (λ t1 t2,
   match t1, t2 with
   | NMap x t1, NMap y t2 => cast_if_and (decide (x = y)) (decide (t1 = t2))
-  end; abstract congruence.
+  end); abstract congruence.
 Defined.
 Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
 Global Opaque Nempty.
diff --git a/prelude/numbers.v b/prelude/numbers.v
index 8abbf502b397e7b8f8387e293fdb0e9575ac03fd..05c66b45896c4f4a9b90dce20041f37fb99c2c8a 100644
--- a/prelude/numbers.v
+++ b/prelude/numbers.v
@@ -9,7 +9,7 @@ From iris.prelude Require Export base decidable option.
 Open Scope nat_scope.
 
 Coercion Z.of_nat : nat >-> Z.
-Instance comparison_eq_dec (c1 c2 : comparison) : Decision (c1 = c2).
+Instance comparison_eq_dec : EqDecision comparison.
 Proof. solve_decision. Defined.
 
 (** * Notations and properties of [nat] *)
@@ -35,13 +35,13 @@ Infix "`mod`" := Nat.modulo (at level 35) : nat_scope.
 Infix "`max`" := Nat.max (at level 35) : nat_scope.
 Infix "`min`" := Nat.min (at level 35) : nat_scope.
 
-Instance nat_eq_dec: ∀ x y : nat, Decision (x = y) := eq_nat_dec.
+Instance nat_eq_dec: EqDecision nat := eq_nat_dec.
 Instance nat_le_dec: ∀ x y : nat, Decision (x ≤ y) := le_dec.
 Instance nat_lt_dec: ∀ x y : nat, Decision (x < y) := lt_dec.
 Instance nat_inhabited: Inhabited nat := populate 0%nat.
-Instance: Inj (=) (=) S.
+Instance S_inj: Inj (=) (=) S.
 Proof. by injection 1. Qed.
-Instance: PartialOrder (≤).
+Instance nat_le_po: PartialOrder (≤).
 Proof. repeat split; repeat intro; auto with lia. Qed.
 
 Instance nat_le_pi: ∀ x y : nat, ProofIrrel (x ≤ y).
@@ -116,7 +116,7 @@ Notation "(~1)" := xI (only parsing) : positive_scope.
 Arguments Pos.of_nat : simpl never.
 Arguments Pmult : simpl never.
 
-Instance positive_eq_dec: ∀ x y : positive, Decision (x = y) := Pos.eq_dec.
+Instance positive_eq_dec: EqDecision positive := Pos.eq_dec.
 Instance positive_inhabited: Inhabited positive := populate 1.
 
 Instance maybe_xO : Maybe xO := λ p, match p with p~0 => Some p | _ => None end.
@@ -198,7 +198,7 @@ Arguments N.add _ _ : simpl never.
 Instance: Inj (=) (=) Npos.
 Proof. by injection 1. Qed.
 
-Instance N_eq_dec: ∀ x y : N, Decision (x = y) := N.eq_dec.
+Instance N_eq_dec: EqDecision N := N.eq_dec.
 Program Instance N_le_dec (x y : N) : Decision (x ≤ y)%N :=
   match Ncompare x y with Gt => right _ | _ => left _ end.
 Solve Obligations with naive_solver.
@@ -206,7 +206,7 @@ Program Instance N_lt_dec (x y : N) : Decision (x < y)%N :=
   match Ncompare x y with Lt => left _ | _ => right _ end.
 Solve Obligations with naive_solver.
 Instance N_inhabited: Inhabited N := populate 1%N.
-Instance: PartialOrder (≤)%N.
+Instance N_le_po: PartialOrder (≤)%N.
 Proof.
   repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
 Qed.
@@ -239,11 +239,11 @@ Proof. by injection 1. Qed.
 Instance Z_of_nat_inj : Inj (=) (=) Z.of_nat.
 Proof. intros n1 n2. apply Nat2Z.inj. Qed.
 
-Instance Z_eq_dec: ∀ x y : Z, Decision (x = y) := Z.eq_dec.
+Instance Z_eq_dec: EqDecision Z := Z.eq_dec.
 Instance Z_le_dec: ∀ x y : Z, Decision (x ≤ y) := Z_le_dec.
 Instance Z_lt_dec: ∀ x y : Z, Decision (x < y) := Z_lt_dec.
 Instance Z_inhabited: Inhabited Z := populate 1.
-Instance Z_le_order : PartialOrder (≤).
+Instance Z_le_po : PartialOrder (≤).
 Proof.
   repeat split; red. apply Z.le_refl. apply Z.le_trans. apply Z.le_antisymm.
 Qed.
@@ -345,7 +345,7 @@ Notation "(<)" := Qclt (only parsing) : Qc_scope.
 Hint Extern 1 (_ ≤ _) => reflexivity || discriminate.
 Arguments Qred _ : simpl never.
 
-Instance Qc_eq_dec: ∀ x y : Qc, Decision (x = y) := Qc_eq_dec.
+Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
 Program Instance Qc_le_dec (x y : Qc) : Decision (x ≤ y) :=
   if Qclt_le_dec y x then right _ else left _.
 Next Obligation. intros x y; apply Qclt_not_le. Qed.
diff --git a/prelude/option.v b/prelude/option.v
index 0f972ca16d9d20d29fb18feb0e59d4e0b56261b2..0ceac790cc6bc3b1284120550c52d6c494a07eab 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -148,14 +148,13 @@ Instance option_eq_None_dec {A} (mx : option A) : Decision (mx = None) :=
   match mx with Some _ => right (Some_ne_None _) | None => left eq_refl end.
 Instance option_None_eq_dec {A} (mx : option A) : Decision (None = mx) :=
   match mx with Some _ => right (None_ne_Some _) | None => left eq_refl end.
-Instance option_eq_dec {A} {dec : ∀ x y : A, Decision (x = y)}
-  (mx my : option A) : Decision (mx = my).
+Instance option_eq_dec `{dec : EqDecision A} : EqDecision (option A).
 Proof.
- refine
+ refine (λ mx my,
   match mx, my with
   | Some x, Some y => cast_if (decide (x = y))
   | None, None => left _ | _, _ => right _
-  end; clear dec; abstract congruence.
+  end); clear dec; abstract congruence.
 Defined.
 
 (** * Monadic operations *)
diff --git a/prelude/orders.v b/prelude/orders.v
index b4d48015619660cf2d4abcda62927a5d4242e842..b3856cee4b01f7118bd12c01eddf720fcd09f840 100644
--- a/prelude/orders.v
+++ b/prelude/orders.v
@@ -48,10 +48,9 @@ Section orders.
     - intros [? HYX]. split. done. by intros <-.
     - intros [? HXY]. split. done. by contradict HXY; apply (anti_symm R).
   Qed.
-  Lemma po_eq_dec `{!PartialOrder R, ∀ X Y, Decision (X ⊆ Y)} (X Y : A) :
-    Decision (X = Y).
+  Lemma po_eq_dec `{!PartialOrder R, ∀ X Y, Decision (X ⊆ Y)} : EqDecision A.
   Proof.
-    refine (cast_if_and (decide (X ⊆ Y)) (decide (Y ⊆ X)));
+    refine (λ X Y, cast_if_and (decide (X ⊆ Y)) (decide (Y ⊆ X)));
      abstract (rewrite anti_symm_iff; tauto).
   Defined.
   Lemma total_not `{!Total R} X Y : X ⊈ Y → Y ⊆ X.
diff --git a/prelude/pmap.v b/prelude/pmap.v
index 483eac8b16690b182496e9510a4b4bb44acd2709..a558d72c65aa546f25266ac2f3b27c4e043bfd7b 100644
--- a/prelude/pmap.v
+++ b/prelude/pmap.v
@@ -26,8 +26,7 @@ Inductive Pmap_raw (A : Type) : Type :=
 Arguments PLeaf {_}.
 Arguments PNode {_} _ _ _.
 
-Instance Pmap_raw_eq_dec `{∀ x y : A, Decision (x = y)} (x y : Pmap_raw A) :
-  Decision (x = y).
+Instance Pmap_raw_eq_dec `{EqDecision A} : EqDecision (Pmap_raw A).
 Proof. solve_decision. Defined.
 
 Fixpoint Pmap_wf {A} (t : Pmap_raw A) : bool :=
@@ -266,8 +265,7 @@ Proof.
   split; [by intros ->|intros]; destruct m1 as [t1 ?], m2 as [t2 ?].
   simplify_eq/=; f_equal; apply proof_irrel.
 Qed.
-Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)}
-    (m1 m2 : Pmap A) : Decision (m1 = m2) :=
+Instance Pmap_eq_dec `{EqDecision A} : EqDecision (Pmap A) := λ m1 m2,
   match Pmap_raw_eq_dec (pmap_car m1) (pmap_car m2) with
   | left H => left (proj2 (Pmap_eq m1 m2) H)
   | right H => right (H ∘ proj1 (Pmap_eq m1 m2))
diff --git a/prelude/strings.v b/prelude/strings.v
index d935c8ed6bbdcf86c09abb2d8c8f35ab81a92ec6..acf0c2c462ea8bf1699d2fa9488baf9bf3efdea1 100644
--- a/prelude/strings.v
+++ b/prelude/strings.v
@@ -16,10 +16,10 @@ Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
 Arguments String.append _ _ : simpl never.
 
 (** * Decision of equality *)
-Instance assci_eq_dec : ∀ a1 a2, Decision (a1 = a2) := ascii_dec.
-Instance string_eq_dec (s1 s2 : string) : Decision (s1 = s2).
+Instance assci_eq_dec : EqDecision ascii := ascii_dec.
+Instance string_eq_dec : EqDecision string.
 Proof. solve_decision. Defined.
-Instance: Inj (=) (=) (String.append s1).
+Instance string_app_inj : Inj (=) (=) (String.append s1).
 Proof. intros s1 ???. induction s1; simplify_eq/=; f_equal/=; auto. Qed.
 
 (* Reverse *)
diff --git a/prelude/vector.v b/prelude/vector.v
index 9253a797f7b162ac3f5681259f1284d682564851..3e32c2a691e3d595f085d52df959dea579fe9ac2 100644
--- a/prelude/vector.v
+++ b/prelude/vector.v
@@ -35,7 +35,7 @@ Coercion fin_to_nat : fin >-> nat.
 Notation fin_of_nat := Fin.of_nat_lt.
 Notation fin_rect2 := Fin.rect2.
 
-Instance fin_dec {n} : ∀ i j : fin n, Decision (i = j).
+Instance fin_dec {n} : EqDecision (fin n).
 Proof.
  refine (fin_rect2
   (λ n (i j : fin n), { i = j } + { i ≠ j })
@@ -163,8 +163,7 @@ Proof.
   - apply IH. intros i. apply (Hi (FS i)).
 Qed.
 
-Instance vec_dec {A} {dec : ∀ x y : A, Decision (x = y)} {n} :
-  ∀ v w : vec A n, Decision (v = w).
+Instance vec_dec {A} {dec : EqDecision A} {n} : EqDecision (vec A n).
 Proof.
  refine (vec_rect2
   (λ n (v w : vec A n), { v = w } + { v ≠ w })
diff --git a/prelude/zmap.v b/prelude/zmap.v
index 238fadc46c63d485cb2a4077ff7a1acfcd34fe18..0d2cea6d4c19aaab0c4abccc0e6beeb50c5ca401 100644
--- a/prelude/zmap.v
+++ b/prelude/zmap.v
@@ -13,14 +13,13 @@ Arguments Zmap_pos {_} _.
 Arguments Zmap_neg {_} _.
 Arguments ZMap {_} _ _ _.
 
-Instance Zmap_eq_dec `{∀ x y : A, Decision (x = y)} (t1 t2 : Zmap A) :
-  Decision (t1 = t2).
+Instance Zmap_eq_dec `{EqDecision A} : EqDecision (Zmap A).
 Proof.
- refine
+ refine (λ t1 t2,
   match t1, t2 with
   | ZMap x t1 t1', ZMap y t2 t2' =>
      cast_if_and3 (decide (x = y)) (decide (t1 = t2)) (decide (t1' = t2'))
-  end; abstract congruence.
+  end); abstract congruence.
 Defined.
 Instance Zempty {A} : Empty (Zmap A) := ZMap None ∅ ∅.
 Instance Zlookup {A} : Lookup Z A (Zmap A) := λ i t,
diff --git a/program_logic/namespaces.v b/program_logic/namespaces.v
index 51093e7f59107e6b2b1c7e122d9a9c350951ab98..62de7e675a7c276c1ba2a9c1544b1e17739372f6 100644
--- a/program_logic/namespaces.v
+++ b/program_logic/namespaces.v
@@ -2,7 +2,7 @@ From iris.prelude Require Export countable coPset.
 From iris.algebra Require Export base.
 
 Definition namespace := list positive.
-Instance namespace_dec (N1 N2 : namespace) : Decision (N1 = N2) := _.
+Instance namespace_eq_dec : EqDecision namespace := _.
 Instance namespace_countable : Countable namespace := _.
 Typeclasses Opaque namespace.