diff --git a/theories/base.v b/theories/base.v
index 464ba6db41011eba7786f47ee8f03aee0c641bcf..f4a76923809bc90be5bd7d5230346410ed2106fb 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -897,6 +897,9 @@ 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.
 
+Notation "x ∉@{ B } X" := (¬x ∈@{B} X) (at level 80, only parsing) : stdpp_scope.
+Notation "(∉@{ B } )" := (λ x X, x ∉@{B} X) (only parsing) : stdpp_scope.
+
 Class Disjoint A := disjoint : A → A → Prop.
  Hint Mode Disjoint ! : typeclass_instances.
 Instance: Params (@disjoint) 2 := {}.
@@ -1136,15 +1139,15 @@ Note that we cannot use the name [Set] since that is a reserved keyword. Hence
 we use [Set_]. *)
 Class SemiSet A C `{ElemOf A C,
     Empty C, Singleton A C, Union C} : Prop := {
-  not_elem_of_empty (x : A) : x ∉ ∅;
-  elem_of_singleton (x y : A) : x ∈ {[ y ]} ↔ x = y;
-  elem_of_union X Y (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
+  not_elem_of_empty (x : A) : x ∉@{C} ∅;
+  elem_of_singleton (x y : A) : x ∈@{C} {[ y ]} ↔ x = y;
+  elem_of_union (X Y : C) (x : A) : x ∈ X ∪ Y ↔ x ∈ X ∨ x ∈ Y
 }.
 Class Set_ A C `{ElemOf A C, Empty C, Singleton A C,
     Union C, Intersection C, Difference C} : Prop := {
   set_semi_set :>> SemiSet A C;
-  elem_of_intersection X Y (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
-  elem_of_difference X Y (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
+  elem_of_intersection (X Y : C) (x : A) : x ∈ X ∩ Y ↔ x ∈ X ∧ x ∈ Y;
+  elem_of_difference (X Y : C) (x : A) : x ∈ X ∖ Y ↔ x ∈ X ∧ x ∉ Y
 }.
 
 (** We axiomative a finite set as a set whose elements can be
@@ -1183,8 +1186,8 @@ anyway so as to avoid cycles in type class search. *)
 Class FinSet A C `{ElemOf A C, Empty C, Singleton A C, Union C,
     Intersection C, Difference C, Elements A C, EqDecision A} : Prop := {
   fin_set_set :>> Set_ A C;
-  elem_of_elements X x : x ∈ elements X ↔ x ∈ X;
-  NoDup_elements X : NoDup (elements X)
+  elem_of_elements (X : C) x : x ∈ elements X ↔ x ∈ X;
+  NoDup_elements (X : C) : NoDup (elements X)
 }.
 Class Size C := size: C → nat.
 Hint Mode Size ! : typeclass_instances.
@@ -1205,10 +1208,11 @@ Class MonadSet M `{∀ A, ElemOf A (M A),
   monad_set_semi_set A :> SemiSet A (M A);
   elem_of_bind {A B} (f : A → M B) (X : M A) (x : B) :
     x ∈ X ≫= f ↔ ∃ y, x ∈ f y ∧ y ∈ X;
-  elem_of_ret {A} (x y : A) : x ∈ mret y ↔ x = y;
+  elem_of_ret {A} (x y : A) : x ∈@{M A} mret y ↔ x = y;
   elem_of_fmap {A B} (f : A → B) (X : M A) (x : B) :
     x ∈ f <$> X ↔ ∃ y, x = f y ∧ y ∈ X;
-  elem_of_join {A} (X : M (M A)) (x : A) : x ∈ mjoin X ↔ ∃ Y, x ∈ Y ∧ Y ∈ X
+  elem_of_join {A} (X : M (M A)) (x : A) :
+    x ∈ mjoin X ↔ ∃ Y : M A, x ∈ Y ∧ Y ∈ X
 }.
 
 (** The [Infinite A] class axiomatizes types [A] with infinitely many elements.
@@ -1255,7 +1259,7 @@ Notation "(⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
 Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
 Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
 
-Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑) := {}.
+Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
 
 Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
diff --git a/theories/coPset.v b/theories/coPset.v
index 4b583ed71d7c9086bd945fa1e748879130d06151..86f723239afcae86e6ef1a9246d01ea46f216dd7 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -318,7 +318,7 @@ Proof.
 Qed.
 
 (** * Conversion to and from gsets of positives *)
-Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf (K:=positive) m.
+Lemma coPset_to_gset_wf (m : Pmap ()) : gmap_wf positive m.
 Proof. done. Qed.
 Definition coPset_to_gset (X : coPset) : gset positive :=
   let 'Mapset m := coPset_to_Pset X in
diff --git a/theories/countable.v b/theories/countable.v
index 721b77aace93fe49686820242e43b740cb095cfa..5f41b827d7b40e745117fe7c9f8f5bd86b74cc65 100644
--- a/theories/countable.v
+++ b/theories/countable.v
@@ -18,14 +18,14 @@ Definition encode_nat `{Countable A} (x : A) : nat :=
   pred (Pos.to_nat (encode x)).
 Definition decode_nat `{Countable A} (i : nat) : option A :=
   decode (Pos.of_nat (S i)).
-Instance encode_inj `{Countable A} : Inj (=) (=) encode.
+Instance encode_inj `{Countable A} : Inj (=) (=) (encode (A:=A)).
 Proof.
   intros x y Hxy; apply (inj Some).
   by rewrite <-(decode_encode x), Hxy, decode_encode.
 Qed.
-Instance encode_nat_inj `{Countable A} : Inj (=) (=) encode_nat.
+Instance encode_nat_inj `{Countable A} : Inj (=) (=) (encode_nat (A:=A)).
 Proof. unfold encode_nat; intros x y Hxy; apply (inj encode); lia. Qed.
-Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x.
+Lemma decode_encode_nat `{Countable A} (x : A) : decode_nat (encode_nat x) = Some x.
 Proof.
   pose proof (Pos2Nat.is_pos (encode x)).
   unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
diff --git a/theories/fin_map_dom.v b/theories/fin_map_dom.v
index d020c1941639122aa4f2614156325a9ec1e059a0..3de5e3e07fcfb652e826be4604b95688bc2baa39 100644
--- a/theories/fin_map_dom.v
+++ b/theories/fin_map_dom.v
@@ -145,12 +145,12 @@ Proof. unfold_leibniz; apply dom_fmap. Qed.
 End fin_map_dom.
 
 Lemma dom_seq `{FinMapDom nat M D} {A} start (xs : list A) :
-  dom D (map_seq start xs) ≡ set_seq start (length xs).
+  dom D (map_seq start (M:=M A) xs) ≡ set_seq start (length xs).
 Proof.
   revert start. induction xs as [|x xs IH]; intros start; simpl.
   - by rewrite dom_empty.
   - by rewrite dom_insert, IH.
 Qed.
 Lemma dom_seq_L `{FinMapDom nat M D, !LeibnizEquiv D} {A} start (xs : list A) :
-  dom D (map_seq start xs) = set_seq start (length xs).
+  dom D (map_seq (M:=M A) start xs) = set_seq start (length xs).
 Proof. unfold_leibniz. apply dom_seq. Qed.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index e31e8d6b34aa6fc3ae460fcbb2819a898e9815dc..6c7270a3ed045d669e8f43273c957bdc544a653d 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -42,8 +42,10 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
   NoDup_map_to_list {A} (m : M A) : NoDup (map_to_list m);
   elem_of_map_to_list {A} (m : M A) i x :
     (i,x) ∈ map_to_list m ↔ m !! i = Some x;
-  lookup_omap {A B} (f : A → option B) m i : omap f m !! i = m !! i ≫= f;
-  lookup_merge {A B C} (f: option A → option B → option C) `{!DiagNone f} m1 m2 i :
+  lookup_omap {A B} (f : A → option B) (m : M A) i :
+    omap f m !! i = m !! i ≫= f; 
+  lookup_merge {A B C} (f : option A → option B → option C)
+      `{!DiagNone f} (m1 : M A) (m2 : M B) i :
     merge f m1 m2 !! i = f (m1 !! i) (m2 !! i)
 }.
 
@@ -943,7 +945,7 @@ Proof.
 Qed.
 
 Lemma elem_of_map_to_set_pair `{FinSet (K * A) C} (m : M A) i x :
-  (i,x) ∈ map_to_set pair m ↔ m !! i = Some x.
+  (i,x) ∈@{C} map_to_set pair m ↔ m !! i = Some x.
 Proof. rewrite elem_of_map_to_set. naive_solver. Qed.
 
 (** ** Induction principles *)
diff --git a/theories/finite.v b/theories/finite.v
index c81b84462340f8b5e1de1eb4b1625a0cbf18f6cd..4d8aba1fe051258a97560730152a0a299dc48025 100644
--- a/theories/finite.v
+++ b/theories/finite.v
@@ -33,7 +33,7 @@ Hint Immediate finite_countable : typeclass_instances.
 Definition find `{Finite A} P `{∀ x, Decision (P x)} : option A :=
   list_find P (enum A) ≫= decode_nat ∘ fst.
 
-Lemma encode_lt_card `{finA: Finite A} x : encode_nat x < card A.
+Lemma encode_lt_card `{finA: Finite A} (x : A) : encode_nat x < card A.
 Proof.
   destruct finA as [xs Hxs HA]; unfold encode_nat, encode, card; simpl.
   rewrite Nat2Pos.id by done; simpl.
@@ -42,7 +42,7 @@ Proof.
   - destruct xs; simpl. exfalso; eapply not_elem_of_nil, (HA x). lia.
 Qed.
 Lemma encode_decode A `{finA: Finite A} i :
-  i < card A → ∃ x, decode_nat i = Some x ∧ encode_nat x = i.
+  i < card A → ∃ x : A, decode_nat i = Some x ∧ encode_nat x = i.
 Proof.
   destruct finA as [xs Hxs HA].
   unfold encode_nat, decode_nat, encode, decode, card; simpl.
@@ -52,7 +52,7 @@ Proof.
   destruct (list_find_Some (x =) xs j y) as [? ->]; auto.
   rewrite Hj; csimpl; eauto using NoDup_lookup.
 Qed.
-Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
+Lemma find_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
   find P = Some x → P x.
 Proof.
   destruct finA as [xs Hxs HA]; unfold find, decode_nat, decode; simpl.
@@ -60,7 +60,7 @@ Proof.
   rewrite !Nat2Pos.id in Hx by done.
   destruct (list_find_Some P xs i y); naive_solver.
 Qed.
-Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} x :
+Lemma find_is_Some `{finA: Finite A} P `{∀ x, Decision (P x)} (x : A) :
   P x → ∃ y, find P = Some y ∧ P y.
 Proof.
   destruct finA as [xs Hxs HA]; unfold find, decode; simpl.
@@ -309,7 +309,7 @@ Definition list_enum {A} (l : list A) : ∀ n, list { l : list A | length l = n
   | S n => foldr (λ x, (sig_map (x ::) (λ _ H, f_equal S H) <$> (go n) ++)) [] l
   end.
 
-Program Instance list_finite `{Finite A} n : Finite { l | length l = n } :=
+Program Instance list_finite `{Finite A} n : Finite { l : list A | length l = n } :=
   {| enum := list_enum (enum A) n |}.
 Next Obligation.
   intros ????. induction n as [|n IH]; simpl; [apply NoDup_singleton |].
@@ -335,7 +335,7 @@ Next Obligation.
   - rewrite elem_of_app. eauto.
 Qed.
 
-Lemma list_card `{Finite A} n : card { l | length l = n } = card A ^ n.
+Lemma list_card `{Finite A} n : card { l : list A | length l = n } = card A ^ n.
 Proof.
   unfold card; simpl. induction n as [|n IH]; simpl; auto.
   rewrite <-IH. clear IH. generalize (list_enum (enum A) n).
diff --git a/theories/gmap.v b/theories/gmap.v
index 4de585769b4401c1e22b2df1b72dc74724981915..c98df62b9e2536e103f66408290b6c57646fbbeb 100644
--- a/theories/gmap.v
+++ b/theories/gmap.v
@@ -9,11 +9,11 @@ From stdpp Require Import pmap mapset propset.
 (** * The data structure *)
 (** We pack a [Pmap] together with a proof that ensures that all keys correspond
 to codes of actual elements of the countable type. *)
-Definition gmap_wf `{Countable K} {A} : Pmap A → Prop :=
-  map_Forall (λ p _, encode <$> decode p = Some p).
+Definition gmap_wf K `{Countable K} {A} : Pmap A → Prop :=
+  map_Forall (λ p _, encode (A:=K) <$> decode p = Some p).
 Record gmap K `{Countable K} A := GMap {
   gmap_car : Pmap A;
-  gmap_prf : bool_decide (gmap_wf gmap_car)
+  gmap_prf : bool_decide (gmap_wf K gmap_car)
 }.
 Arguments GMap {_ _ _ _} _ _ : assert.
 Arguments gmap_car {_ _ _ _} _ : assert.
@@ -35,7 +35,7 @@ Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
 Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
 Global Opaque gmap_empty.
 Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
-  gmap_wf m → gmap_wf (partial_alter f (encode i) m).
+  gmap_wf K m → gmap_wf K (partial_alter f (encode (A:=K) i) m).
 Proof.
   intros Hm p x. destruct (decide (encode i = p)) as [<-|?].
   - rewrite decode_encode; eauto.
@@ -47,13 +47,13 @@ Instance gmap_partial_alter `{Countable K} {A} :
     (bool_decide_pack _ (gmap_partial_alter_wf f m i
     (bool_decide_unpack _ Hm))).
 Lemma gmap_fmap_wf `{Countable K} {A B} (f : A → B) m :
-  gmap_wf m → gmap_wf (f <$> m).
+  gmap_wf K m → gmap_wf K (f <$> m).
 Proof. intros ? p x. rewrite lookup_fmap, fmap_Some; intros (?&?&?); eauto. Qed.
 Instance gmap_fmap `{Countable K} : FMap (gmap K) := λ A B f m,
   let (m,Hm) := m in GMap (f <$> m)
     (bool_decide_pack _ (gmap_fmap_wf f m (bool_decide_unpack _ Hm))).
 Lemma gmap_omap_wf `{Countable K} {A B} (f : A → option B) m :
-  gmap_wf m → gmap_wf (omap f m).
+  gmap_wf K m → gmap_wf K (omap f m).
 Proof. intros ? p x; rewrite lookup_omap, bind_Some; intros (?&?&?); eauto. Qed.
 Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f m,
   let (m,Hm) := m in GMap (omap f m)
@@ -61,7 +61,7 @@ Instance gmap_omap `{Countable K} : OMap (gmap K) := λ A B f m,
 Lemma gmap_merge_wf `{Countable K} {A B C}
     (f : option A → option B → option C) m1 m2 :
   let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
-  gmap_wf m1 → gmap_wf m2 → gmap_wf (merge f' m1 m2).
+  gmap_wf K m1 → gmap_wf K m2 → gmap_wf K (merge f' m1 m2).
 Proof.
   intros f' Hm1 Hm2 p z; rewrite lookup_merge by done; intros.
   destruct (m1 !! _) eqn:?, (m2 !! _) eqn:?; naive_solver.