diff --git a/algebra/gmap.v b/algebra/gmap.v
index c0e59099a938be9bfa46d84683d27cbc8e32a458..b7884958ee7c92df1b199aa04e544a125aca41a4 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -47,7 +47,7 @@ Proof.
   by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
 Qed.
 Global Instance insert_ne i n :
-  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
+  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K) i).
 Proof.
   intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
     [by constructor|by apply lookup_ne].
@@ -56,7 +56,7 @@ Global Instance singleton_ne i n :
   Proper (dist n ==> dist n) (singletonM i : A → gmap K A).
 Proof. by intros ???; apply insert_ne. Qed.
 Global Instance delete_ne i n :
-  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
+  Proper (dist n ==> dist n) (delete (M:=gmap K) i).
 Proof.
   intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
     [by constructor|by apply lookup_ne].
@@ -183,10 +183,12 @@ Arguments gmapUR _ {_ _} _.
 Section properties.
 Context `{Countable K} {A : cmraT}.
 Implicit Types m : gmap K A.
+Implicit Types mm : option (gmap K A).
 Implicit Types i : K.
 Implicit Types x y : A.
 
-Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
+Lemma lookup_opM m1 mm2 i :
+  (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i) : option A).
 Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
 
 Lemma lookup_validN_Some n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x.
@@ -343,7 +345,8 @@ Section freshness.
 End freshness.
 
 Lemma insert_local_update m i x y mf :
-  x ~l~> y @ mf ≫= (!! i) → <[i:=x]>m ~l~> <[i:=y]>m @ mf.
+  x ~l~> y @ mf ≫= (!! i) →
+  (<[i:=x]>m : gmap K A) ~l~> <[i:=y]>m @ mf.
 Proof.
   intros [Hxy Hxy']; split.
   - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
@@ -356,7 +359,8 @@ Proof.
 Qed.
 
 Lemma singleton_local_update i x y mf :
-  x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf.
+  x ~l~> y @ mf ≫= (!! i) →
+  ({[ i := x ]} : gmap K A) ~l~> {[ i := y ]} @ mf.
 Proof. apply insert_local_update. Qed.
 
 Lemma alloc_singleton_local_update m i x mf :
@@ -371,7 +375,8 @@ Proof.
 Qed.
 
 Lemma alloc_unit_singleton_local_update i x mf :
-  mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf.
+  mf ≫= (!! i) = None → ✓ x →
+  (∅:gmap K A) ~l~> {[ i := x ]} @ mf.
 Proof.
   intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
 Qed.
diff --git a/algebra/list.v b/algebra/list.v
index 3ab4d27c259f3b75a130ae1163f0814ff01d522b..415af331587e96d56d2d7e3f977ce0c0b5eb36a1 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -17,17 +17,17 @@ Global Instance tail_ne n : Proper (dist n ==> dist n) (@tail A) := _.
 Global Instance take_ne n : Proper (dist n ==> dist n) (@take A n) := _.
 Global Instance drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _.
 Global Instance list_lookup_ne n i :
-  Proper (dist n ==> dist n) (lookup (M:=list A) i).
+  Proper (dist n ==> dist n) (lookup (M:=list) i).
 Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
 Global Instance list_alter_ne n f i :
   Proper (dist n ==> dist n) f →
-  Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
+  Proper (dist n ==> dist n) (alter (M:=list) f i) := _.
 Global Instance list_insert_ne n i :
-  Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _.
+  Proper (dist n ==> dist n ==> dist n) (insert (M:=list) i) := _.
 Global Instance list_inserts_ne n i :
   Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _.
 Global Instance list_delete_ne n i :
-  Proper (dist n ==> dist n) (delete (M:=list A) i) := _.
+  Proper (dist n ==> dist n) (delete (M:=list) i) := _.
 Global Instance option_list_ne n : Proper (dist n ==> dist n) (@option_list A).
 Proof. intros ???; by apply Forall2_option_list, dist_option_Forall2. Qed.
 Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
@@ -236,17 +236,20 @@ End cmra.
 Arguments listR : clear implicits.
 Arguments listUR : clear implicits.
 
-Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
+Definition list_singleton {A : ucmraT} (n : nat) (x : A) : list A :=
   replicate n ∅ ++ [x].
 
 Section properties.
   Context {A : ucmraT}.
-  Implicit Types l : list A.
+  Implicit Types l k : list A.
+  Implicit Types ml mk : option (list A).
   Implicit Types x y z : A.
+  Implicit Types i : nat.
   Local Arguments op _ _ !_ !_ / : simpl nomatch.
   Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
 
-  Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i)).
+  Lemma list_lookup_opM l mk i :
+    (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i) : option A).
   Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.
 
   Lemma list_op_app l1 l2 l3 :
@@ -266,57 +269,52 @@ Section properties.
 
   Lemma replicate_valid n (x : A) : ✓ x → ✓ replicate n x.
   Proof. apply Forall_replicate. Qed.
-  Global Instance list_singletonM_ne n i :
-    Proper (dist n ==> dist n) (@list_singletonM A i).
+  Global Instance list_singleton_ne n i :
+    Proper (dist n ==> dist n) (@list_singleton A i).
   Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
-  Global Instance list_singletonM_proper i :
-    Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
+  Global Instance list_singleton_proper i :
+    Proper ((≡) ==> (≡)) (list_singleton i) := ne_proper _.
 
-  Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x.
+  Lemma elem_of_list_singleton i z x : z ∈ list_singleton i x → z = ∅ ∨ z = x.
   Proof.
     rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
   Qed.
-  Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x.
+  Lemma list_lookup_singleton i x : list_singleton i x !! i = Some x.
   Proof. induction i; by f_equal/=. Qed.
-  Lemma list_lookup_singletonM_ne i j x :
-    i ≠ j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅.
+  Lemma list_lookup_singleton_ne i j x :
+    i ≠ j → list_singleton i x !! j = None ∨ list_singleton i x !! j = Some ∅.
   Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
-  Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x.
+  Lemma list_singleton_validN n i x : ✓{n} (list_singleton i x) ↔ ✓{n} x.
   Proof.
     rewrite list_lookup_validN. split.
-    { move=> /(_ i). by rewrite list_lookup_singletonM. }
+    { move=> /(_ i). by rewrite list_lookup_singleton. }
     intros Hx j; destruct (decide (i = j)); subst.
-    - by rewrite list_lookup_singletonM.
-    - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
+    - by rewrite list_lookup_singleton.
+    - destruct (list_lookup_singleton_ne i j x) as [Hi|Hi]; first done;
         rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
   Qed.
-  Lemma list_singleton_valid  i x : ✓ {[ i := x ]} ↔ ✓ x.
-  Proof.
-    rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
-  Qed.
-  Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
+  Lemma list_singleton_valid  i x : ✓ (list_singleton i x) ↔ ✓ x.
   Proof.
-    rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
+    rewrite !cmra_valid_validN. by setoid_rewrite list_singleton_validN.
   Qed.
+  Lemma list_singleton_length i x : length (list_singleton i x) = S i.
+  Proof. rewrite /list_singleton app_length replicate_length /=; lia. Qed.
 
-  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
+  Lemma list_core_singleton i x :
+    core (list_singleton i x) ≡ list_singleton i (core x).
   Proof.
-    rewrite /singletonM /list_singletonM.
+    rewrite /list_singleton.
     by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ∅).
   Qed.
-  Lemma list_op_singletonM i (x y : A) :
-    {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
-  Proof.
-    rewrite /singletonM /list_singletonM /=.
-    induction i; constructor; rewrite ?left_id; auto.
-  Qed.
-  Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}.
-  Proof.
-    rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
-  Qed.
-  Global Instance list_singleton_persistent i (x : A) :
-    Persistent x → Persistent {[ i := x ]}.
-  Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed.
+  Lemma list_op_singleton i x y :
+    list_singleton i x ⋅ list_singleton i y ≡ list_singleton i (x ⋅ y).
+  Proof. induction i; constructor; rewrite ?left_id; auto. Qed.
+  Lemma list_alter_singleton f i x :
+    alter f i (list_singleton i x) = list_singleton i (f x).
+  Proof. rewrite /list_singleton. induction i; f_equal/=; auto. Qed.
+  Global Instance list_singleton_persistent i x :
+    Persistent x → Persistent (list_singleton i x).
+  Proof. by rewrite !persistent_total list_core_singleton=> ->. Qed.
 
   (* Update *)
   Lemma list_middle_updateP (P : A → Prop) (Q : list A → Prop) l1 x l2 :
@@ -362,7 +360,7 @@ Section properties.
   Qed.
 
   Lemma list_singleton_local_update i x y ml :
-    x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
+    x ~l~> y @ ml ≫= (!! i) → list_singleton i x ~l~> list_singleton i y @ ml.
   Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
 End properties.
 
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index 85e2b334696d2fa2a0af9d1c6bee29394ef9840f..fff429f16ed08b3f5961912d87cbefdd83593a5b 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -109,7 +109,9 @@ Proof. induction 1; simpl; auto with I. Qed.
 Section gmap.
   Context `{Countable K} {A : Type}.
   Implicit Types m : gmap K A.
+  Implicit Types i : K.
   Implicit Types Φ Ψ : K → A → uPred M.
+  Implicit Types P : uPred M.
 
   Lemma big_sepM_mono Φ Ψ m1 m2 :
     m2 ⊆ m1 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
@@ -187,16 +189,17 @@ Section gmap.
 
   Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b :
     m !! i = None →
-       ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))
+       ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (fn_insert i b f k))
     ⊣⊢ (Ψ i x b ★ [★ map] k↦y ∈ m, Ψ k y (f k)).
   Proof.
     intros. rewrite big_sepM_insert // fn_lookup_insert.
     apply sep_proper, big_sepM_proper; auto=> k y ?.
     by rewrite fn_lookup_insert_ne; last set_solver.
   Qed.
+
   Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
     m !! i = None →
-    ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
+    ([★ map] k↦y ∈ <[i:=x]> m, (fn_insert i P Φ k)) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
   Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
 
   Lemma big_sepM_sepM Φ Ψ m :
@@ -300,15 +303,17 @@ Section gset.
   Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
   Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b :
     x ∉ X →
-       ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y))
+       ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (fn_insert x b f y))
     ⊣⊢ (Ψ x b ★ [★ set] y ∈ X, Ψ y (f y)).
   Proof.
     intros. rewrite big_sepS_insert // fn_lookup_insert.
     apply sep_proper, big_sepS_proper; auto=> y ??.
     by rewrite fn_lookup_insert_ne; last set_solver.
   Qed.
+
   Lemma big_sepS_fn_insert' Φ X x P :
-    x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y).
+    x ∉ X →
+    ([★ set] y ∈ {[ x ]} ∪ X, fn_insert x P Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y).
   Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
 
   Lemma big_sepS_delete Φ X x :
diff --git a/heap_lang/lib/barrier/proof.v b/heap_lang/lib/barrier/proof.v
index 879ac67ca45340116ee364ed291821299a213aab..0251c484b40e01d8e6b408d3dfb049bad22b4a90 100644
--- a/heap_lang/lib/barrier/proof.v
+++ b/heap_lang/lib/barrier/proof.v
@@ -82,7 +82,7 @@ Lemma ress_split i i1 i2 Q R1 R2 P I :
 Proof.
   iIntros (????) "(#HQ&#H1&#H2&HQR&H)"; iDestruct "H" as (Ψ) "[HPΨ HΨ]".
   iDestruct (big_sepS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
-  iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
+  iExists (fn_insert i1 R1 (fn_insert i2 R2 Ψ)). iSplitL "HQR HPΨ".
   - iPoseProof (saved_prop_agree i Q (Ψ i) with "[#]") as "Heq"; first by iSplit.
     iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
     iDestruct (big_sepS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 24eb4d3a6c6fe8c986870c08711745eea10f24e1..5edc2f1800a2abbda74bab318c0677a478013b7c 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -11,6 +11,7 @@ Context {Σ : iFunctor}.
 Implicit Types P Q : iProp heap_lang Σ.
 Implicit Types Φ : val → iProp heap_lang Σ.
 Implicit Types ef : option expr.
+Implicit Types l : loc.
 
 (** Bind. This bundles some arguments that wp_ectx_bind leaves as indices. *)
 Lemma wp_bind {E e} K Φ :
@@ -92,19 +93,19 @@ Proof.
     intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_un_op E op l l' Φ :
-  un_op_eval op l = Some l' →
-  ▷ (|={E}=> Φ (LitV l')) ⊢ WP UnOp op (Lit l) @ E {{ Φ }}.
+Lemma wp_un_op E op li li' Φ :
+  un_op_eval op li = Some li' →
+  ▷ (|={E}=> Φ (LitV li')) ⊢ WP UnOp op (Lit li) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit l') None)
+  intros. rewrite -(wp_lift_pure_det_head_step (UnOp op _) (Lit li') None)
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
-Lemma wp_bin_op E op l1 l2 l' Φ :
-  bin_op_eval op l1 l2 = Some l' →
-  ▷ (|={E}=> Φ (LitV l')) ⊢ WP BinOp op (Lit l1) (Lit l2) @ E {{ Φ }}.
+Lemma wp_bin_op E op li1 li2 li' Φ :
+  bin_op_eval op li1 li2 = Some li' →
+  ▷ (|={E}=> Φ (LitV li')) ⊢ WP BinOp op (Lit li1) (Lit li2) @ E {{ Φ }}.
 Proof.
-  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit l') None)
+  intros Heval. rewrite -(wp_lift_pure_det_head_step (BinOp op _ _) (Lit li') None)
     ?right_id -?wp_value_pvs //; intros; inv_head_step; eauto.
 Qed.
 
diff --git a/prelude/base.v b/prelude/base.v
index b046cf8e814a59f69444b04f98611140c266b996..40e58b18e03938ce2d4609b283940333f6b41dfe 100644
--- a/prelude/base.v
+++ b/prelude/base.v
@@ -785,7 +785,7 @@ Notation "'guard' P 'as' H ; o" := (mguard P (λ H, o))
 (** In this section we define operational type classes for the operations
 on maps. In the file [fin_maps] we will axiomatize finite maps.
 The function look up [m !! k] should yield the element at key [k] in [m]. *)
-Class Lookup (K A M : Type) := lookup: K → M → option A.
+Class Lookup (K : Type) (M : Type → Type) := lookup : ∀ {A}, K → M A → option A.
 Instance: Params (@lookup) 4.
 Notation "m !! i" := (lookup i m) (at level 20) : C_scope.
 Notation "(!!)" := lookup (only parsing) : C_scope.
@@ -794,13 +794,14 @@ Notation "(!! i )" := (lookup i) (only parsing) : C_scope.
 Arguments lookup _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The singleton map *)
-Class SingletonM K A M := singletonM: K → A → M.
+Class SingletonM (K : Type) (M : Type → Type) :=
+  singletonM : ∀ {A}, K → A → M A.
 Instance: Params (@singletonM) 5.
 Notation "{[ k := a ]}" := (singletonM k a) (at level 1) : C_scope.
 
 (** The function insert [<[k:=a]>m] should update the element at key [k] with
 value [a] in [m]. *)
-Class Insert (K A M : Type) := insert: K → A → M → M.
+Class Insert (K : Type) (M : Type → Type) := insert : ∀ {A}, K → A → M A → M A.
 Instance: Params (@insert) 5.
 Notation "<[ k := a ]>" := (insert k a)
   (at level 5, right associativity, format "<[ k := a ]>") : C_scope.
@@ -809,13 +810,14 @@ Arguments insert _ _ _ _ !_ _ !_ / : simpl nomatch.
 (** The function delete [delete k m] should delete the value at key [k] in
 [m]. If the key [k] is not a member of [m], the original map should be
 returned. *)
-Class Delete (K M : Type) := delete: K → M → M.
-Instance: Params (@delete) 4.
-Arguments delete _ _ _ !_ !_ / : simpl nomatch.
+Class Delete (K : Type) (M : Type → Type) := delete : ∀ {A}, K → M A → M A.
+Instance: Params (@delete) 5.
+Arguments delete _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [alter f k m] should update the value at key [k] using the
 function [f], which is called with the original value. *)
-Class Alter (K A M : Type) := alter: (A → A) → K → M → M.
+Class Alter (K : Type) (M : Type → Type) :=
+  alter : ∀ {A}, (A → A) → K → M A → M A.
 Instance: Params (@alter) 5.
 Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
 
@@ -823,16 +825,16 @@ Arguments alter {_ _ _ _} _ !_ !_ / : simpl nomatch.
 function [f], which is called with the original value at key [k] or [None]
 if [k] is not a member of [m]. The value at [k] should be deleted if [f] 
 yields [None]. *)
-Class PartialAlter (K A M : Type) :=
-  partial_alter: (option A → option A) → K → M → M.
+Class PartialAlter (K : Type) (M : Type → Type) :=
+  partial_alter : ∀ {A}, (option A → option A) → K → M A → M A.
 Instance: Params (@partial_alter) 4.
 Arguments partial_alter _ _ _ _ _ !_ !_ / : simpl nomatch.
 
 (** The function [dom C m] should yield the domain of [m]. That is a finite
 collection of type [C] that contains the keys that are a member of [m]. *)
-Class Dom (M C : Type) := dom: M → C.
-Instance: Params (@dom) 3.
-Arguments dom {_} _ {_} !_ / : simpl nomatch, clear implicits.
+Class Dom (M : Type → Type) (C : Type) := dom : ∀ {A}, M A → C.
+Instance: Params (@dom) 4.
+Arguments dom {_} _ {_ _} !_ / : simpl nomatch, clear implicits.
 
 (** The function [merge f m1 m2] should merge the maps [m1] and [m2] by
 constructing a new map whose value at key [k] is [f (m1 !! k) (m2 !! k)].*)
@@ -844,39 +846,27 @@ Arguments merge _ _ _ _ _ _ !_ !_ / : simpl nomatch.
 (** The function [union_with f m1 m2] is supposed to yield the union of [m1]
 and [m2] using the function [f] to combine values of members that are in
 both [m1] and [m2]. *)
-Class UnionWith (A M : Type) :=
-  union_with: (A → A → option A) → M → M → M.
+Class UnionWith (M : Type → Type) :=
+  union_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
 Instance: Params (@union_with) 3.
 Arguments union_with {_ _ _} _ !_ !_ / : simpl nomatch.
 
 (** Similarly for intersection and difference. *)
-Class IntersectionWith (A M : Type) :=
-  intersection_with: (A → A → option A) → M → M → M.
+Class IntersectionWith (M : Type → Type) :=
+  intersection_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
 Instance: Params (@intersection_with) 3.
 Arguments intersection_with {_ _ _} _ !_ !_ / : simpl nomatch.
 
-Class DifferenceWith (A M : Type) :=
-  difference_with: (A → A → option A) → M → M → M.
+Class DifferenceWith (M : Type → Type) :=
+  difference_with : ∀ {A}, (A → A → option A) → M A → M A → M A.
 Instance: Params (@difference_with) 3.
 Arguments difference_with {_ _ _} _ !_ !_ / : simpl nomatch.
 
-Definition intersection_with_list `{IntersectionWith A M}
-  (f : A → A → option A) : M → list M → M := fold_right (intersection_with f).
+Definition intersection_with_list `{IntersectionWith M} {A}
+    (f : A → A → option A) : M A → list (M A) → M A :=
+  fold_right (intersection_with f).
 Arguments intersection_with_list _ _ _ _ _ !_ /.
 
-Class LookupE (E K A M : Type) := lookupE: E → K → M → option A.
-Instance: Params (@lookupE) 6.
-Notation "m !!{ Γ } i" := (lookupE Γ i m)
-  (at level 20, format "m  !!{ Γ }  i") : C_scope.
-Notation "(!!{ Γ } )" := (lookupE Γ) (only parsing, Γ at level 1) : C_scope.
-Arguments lookupE _ _ _ _ _ _ !_ !_ / : simpl nomatch.
-
-Class InsertE (E K A M : Type) := insertE: E → K → A → M → M.
-Instance: Params (@insertE) 6.
-Notation "<[ k := a ]{ Γ }>" := (insertE Γ k a)
-  (at level 5, right associativity, format "<[ k := a ]{ Γ }>") : C_scope.
-Arguments insertE _ _ _ _ _ _ !_ _ !_ / : simpl nomatch.
-
 
 (** * Axiomatization of collections *)
 (** The class [SimpleCollection A C] axiomatizes a collection of type [C] with
diff --git a/prelude/coPset.v b/prelude/coPset.v
index 9e37b07d05b7479608af74e3588599e5d1ecc0b7..2a572ec9751db21e624ca262ec84187a9e6d7e6e 100644
--- a/prelude/coPset.v
+++ b/prelude/coPset.v
@@ -326,13 +326,13 @@ Proof.
 Qed.
 
 (** * Domain of finite maps *)
-Instance Pmap_dom_coPset {A} : Dom (Pmap A) coPset := λ m, of_Pset (dom _ m).
+Instance Pmap_dom_coPset : Dom Pmap coPset := λ A m, of_Pset (dom _ m).
 Instance Pmap_dom_coPset_spec: FinMapDom positive Pmap coPset.
 Proof.
   split; try apply _; intros A m i; unfold dom, Pmap_dom_coPset.
   by rewrite elem_of_of_Pset, elem_of_dom.
 Qed.
-Instance gmap_dom_coPset {A} : Dom (gmap positive A) coPset := λ m,
+Instance gmap_dom_coPset : Dom (gmap positive) coPset := λ A m,
   of_gset (dom _ m).
 Instance gmap_dom_coPset_spec: FinMapDom positive (gmap positive) coPset.
 Proof.
diff --git a/prelude/fin_map_dom.v b/prelude/fin_map_dom.v
index afb29ae11ec685fe7e421e7881829156de69dfdb..42d0a40ec4678b4abc1d9fb03f1a1aff78dbdf08 100644
--- a/prelude/fin_map_dom.v
+++ b/prelude/fin_map_dom.v
@@ -5,10 +5,9 @@ maps. We provide such an axiomatization, instead of implementing the domain
 function in a generic way, to allow more efficient implementations. *)
 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),
-    ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D,
+Class FinMapDom K M D `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M,
+    OMap M, Merge M, FinMapToList K M, ∀ i j : K, Decision (i = j),
+    Dom M D, ElemOf K D, Empty D, Singleton K D,
     Union D, Intersection D, Difference D} := {
   finmap_dom_map :>> FinMap K M;
   finmap_dom_collection :>> Collection K D;
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 5f4b4bcae225abf461877c3ff773ae1431d04689..574e2c33463553ee955449916f428e2e5b9d0491 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -23,11 +23,11 @@ prove well founded recursion on finite maps. *)
 which enables us to give a generic implementation of [union_with],
 [intersection_with], and [difference_with]. *)
 
-Class FinMapToList K A M := map_to_list: M → list (K * A).
+Class FinMapToList (K : Type) (M : Type → Type) :=
+  map_to_list : ∀ {A}, M A → 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)} := {
+Class FinMap K M `{FMap M, Lookup K M, ∀ A, Empty (M A), PartialAlter K M,
+    OMap M, Merge M, FinMapToList K M, ∀ i j : K, Decision (i = j)} := {
   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 :
@@ -48,47 +48,47 @@ Class FinMap K M `{FMap M, ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A,
 finite map implementations. These generic implementations do not cause a
 significant performance loss to make including them in the finite map interface
 worthwhile. *)
-Instance map_insert `{PartialAlter K A M} : Insert K A M :=
-  λ i x, partial_alter (λ _, Some x) i.
-Instance map_alter `{PartialAlter K A M} : Alter K A M :=
-  λ f, partial_alter (fmap f).
-Instance map_delete `{PartialAlter K A M} : Delete K M :=
-  partial_alter (λ _, None).
-Instance map_singleton `{PartialAlter K A M, Empty M} :
-  SingletonM K A M := λ i x, <[i:=x]> ∅.
+Instance map_insert `{PartialAlter K M} : Insert K M :=
+  λ A i x, partial_alter (λ _, Some x) i.
+Instance map_alter `{PartialAlter K M} : Alter K M :=
+  λ A f, partial_alter (fmap f).
+Instance map_delete `{PartialAlter K M} : Delete K M :=
+  λ A, partial_alter (λ _, None).
+Instance map_singleton `{PartialAlter K M, ∀ A, Empty (M A)} : SingletonM K M :=
+  λ A i x, <[i:=x]> ∅.
 
-Definition map_of_list `{Insert K A M, Empty M} : list (K * A) → M :=
+Definition map_of_list `{Insert K M, Empty (M A)} : list (K * A) → M A :=
   fold_right (λ p, <[p.1:=p.2]>) ∅.
-Definition map_of_collection `{Elements K C, Insert K A M, Empty M}
-    (f : K → option A) (X : C) : M :=
+Definition map_of_collection `{Elements K C, Insert K M, Empty (M A)}
+    (f : K → option A) (X : C) : M A :=
   map_of_list (omap (λ i, (i,) <$> f i) (elements X)).
 
-Instance map_union_with `{Merge M} {A} : UnionWith A (M A) :=
-  λ f, merge (union_with f).
-Instance map_intersection_with `{Merge M} {A} : IntersectionWith A (M A) :=
-  λ f, merge (intersection_with f).
-Instance map_difference_with `{Merge M} {A} : DifferenceWith A (M A) :=
-  λ f, merge (difference_with f).
+Instance map_union_with `{Merge M} : UnionWith M :=
+  λ A f, merge (union_with f).
+Instance map_intersection_with `{Merge M} : IntersectionWith M :=
+  λ A f, merge (intersection_with f).
+Instance map_difference_with `{Merge M} : DifferenceWith M :=
+  λ A f, merge (difference_with f).
 
-Instance map_equiv `{∀ A, Lookup K A (M A), Equiv A} : Equiv (M A) | 18 :=
+Instance map_equiv `{Lookup K M, Equiv A} : Equiv (M A) | 18 :=
   λ m1 m2, ∀ i, m1 !! i ≡ m2 !! i.
 
 (** The relation [intersection_forall R] on finite maps describes that the
 relation [R] holds for each pair in the intersection. *)
-Definition map_Forall `{Lookup K A M} (P : K → A → Prop) : M → Prop :=
+Definition map_Forall `{Lookup K M} {A} (P : K → A → Prop) : M A → Prop :=
   λ m, ∀ i x, m !! i = Some x → P i x.
-Definition map_relation `{∀ A, Lookup K A (M A)} {A B} (R : A → B → Prop)
+Definition map_relation `{Lookup K M} {A B} (R : A → B → Prop)
     (P : A → Prop) (Q : B → Prop) (m1 : M A) (m2 : M B) : Prop := ∀ i,
   option_relation R P Q (m1 !! i) (m2 !! i).
-Definition map_included `{∀ A, Lookup K A (M A)} {A}
+Definition map_included `{Lookup K M} {A}
   (R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
-Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
+Definition map_disjoint `{Lookup K M} {A} : relation (M A) :=
   map_relation (λ _ _, False) (λ _, True) (λ _, True).
 Infix "⊥ₘ" := map_disjoint (at level 70) : C_scope.
 Hint Extern 0 (_ ⊥ₘ _) => symmetry; eassumption.
 Notation "( m ⊥ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
 Notation "(.⊥ₘ m )" := (λ m2, m2 ⊥ₘ m) (only parsing) : C_scope.
-Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
+Instance map_subseteq `{Lookup K M} {A} : SubsetEq (M A) :=
   map_included (=).
 
 (** The union of two finite maps only has a meaningful definition for maps
@@ -106,8 +106,8 @@ Instance map_difference `{Merge M} {A} : Difference (M A) :=
 
 (** A stronger variant of map that allows the mapped function to use the index
 of the elements. Implemented by conversion to lists, so not very efficient. *)
-Definition map_imap `{∀ A, Insert K A (M A), ∀ A, Empty (M A),
-    ∀ A, FinMapToList K A (M A)} {A B} (f : K → A → option B) (m : M A) : M B :=
+Definition map_imap `{Insert K M, ∀ A, Empty (M A),
+    FinMapToList K M} {A B} (f : K → A → option B) (m : M A) : M B :=
   map_of_list (omap (λ ix, (fst ix,) <$> curry f ix) (map_to_list m)).
 
 (** * Theorems *)
@@ -124,27 +124,25 @@ Section setoid.
     - by intros m1 m2 ? i.
     - by intros m1 m2 m3 ?? i; trans (m2 !! i).
   Qed.
-  Global Instance lookup_proper (i : K) :
-    Proper ((≡) ==> (≡)) (lookup (M:=M A) i).
+  Global Instance lookup_proper (i: K) : Proper ((≡) ==> (≡)) (lookup (M:=M) i).
   Proof. by intros m1 m2 Hm. Qed.
   Global Instance partial_alter_proper :
-    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M A)).
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (partial_alter (M:=M)).
   Proof.
     by intros f1 f2 Hf i ? <- m1 m2 Hm j; destruct (decide (i = j)) as [->|];
       rewrite ?lookup_partial_alter, ?lookup_partial_alter_ne by done;
       try apply Hf; apply lookup_proper.
   Qed.
   Global Instance insert_proper (i : K) :
-    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M A) i).
+    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=M) i).
   Proof. by intros ???; apply partial_alter_proper; [constructor|]. Qed.
-  Global Instance singleton_proper k :
-    Proper ((≡) ==> (≡)) (singletonM k : A → M A).
+  Global Instance singleton_proper (i : K) :
+    Proper ((≡) ==> (≡)) (singletonM (M:=M) i).
   Proof. by intros ???; apply insert_proper. Qed.
-  Global Instance delete_proper (i : K) :
-    Proper ((≡) ==> (≡)) (delete (M:=M A) i).
+  Global Instance delete_proper (i: K) : Proper ((≡) ==> (≡)) (delete (M:=M) i).
   Proof. by apply partial_alter_proper; [constructor|]. Qed.
   Global Instance alter_proper :
-    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (A:=A) (M:=M A)).
+    Proper (((≡) ==> (≡)) ==> (=) ==> (≡) ==> (≡)) (alter (M:=M)).
   Proof.
     intros ?? Hf; apply partial_alter_proper.
     by destruct 1; constructor; apply Hf.
@@ -156,7 +154,7 @@ Section setoid.
     by intros Hf ?? Hm1 ?? Hm2 i; rewrite !lookup_merge by done; apply Hf.
   Qed.
   Global Instance union_with_proper :
-    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M A)).
+    Proper (((≡) ==> (≡) ==> (≡)) ==> (≡) ==> (≡) ==>(≡)) (union_with (M:=M)).
   Proof.
     intros ?? Hf ?? Hm1 ?? Hm2 i; apply (merge_ext _ _); auto.
     by do 2 destruct 1; first [apply Hf | constructor].
diff --git a/prelude/functions.v b/prelude/functions.v
index 935d1b448b9dcbd9c1b62f790e57004b341c2e35..8d401dec052337daf284a3aa5efc35a0f0b279dd 100644
--- a/prelude/functions.v
+++ b/prelude/functions.v
@@ -2,10 +2,10 @@ From iris.prelude Require Export base tactics.
 
 Section definitions.
   Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
-  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) :=
-    λ (g : T → T) a f b, if decide (a = b) then g (f a) else f b.
+  Definition fn_insert (a : A) (t : T) (f : A → T) : A → T := λ b,
+    if decide (a = b) then t else f b.
+  Definition fn_alter (g : T → T) (a : A) (f : A → T) : A → T := λ b,
+    if decide (a = b) then g (f a) else f b.
 End definitions.
 
 (* TODO: For now, we only have the properties here that do not need a notion
@@ -14,17 +14,17 @@ End definitions.
 Section functions.
   Context {A T : Type} `{∀ a b : A, Decision (a = b)}.
 
-  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.
+  Lemma fn_lookup_insert (f : A → T) a t : fn_insert a t f a = t.
+  Proof. unfold fn_insert. by destruct (decide (a = a)). Qed.
   Lemma fn_lookup_insert_rev  (f : A → T) a t1 t2 :
-    <[a:=t1]>f a = t2 → t1 = t2.
+    fn_insert a t1 f a = t2 → t1 = t2.
   Proof. rewrite fn_lookup_insert. congruence. Qed.
-  Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠ b → <[a:=t]>f b = f b.
-  Proof. unfold insert, fn_insert. by destruct (decide (a = b)). Qed.
+  Lemma fn_lookup_insert_ne (f : A → T) a b t : a ≠ b → fn_insert a t f b = f b.
+  Proof. unfold fn_insert. by destruct (decide (a = b)). Qed.
 
-  Lemma fn_lookup_alter (g : T → T) (f : A → T) a : alter g a f a = g (f a).
-  Proof. unfold alter, fn_alter. by destruct (decide (a = a)). Qed.
+  Lemma fn_lookup_alter (g : T → T) (f : A → T) a : fn_alter g a f a = g (f a).
+  Proof. unfold fn_alter. by destruct (decide (a = a)). Qed.
   Lemma fn_lookup_alter_ne (g : T → T) (f : A → T) a b :
-    a ≠ b → alter g a f b = f b.
-  Proof. unfold alter, fn_alter. by destruct (decide (a = b)). Qed.
+    a ≠ b → fn_alter g a f b = f b.
+  Proof. unfold fn_alter. by destruct (decide (a = b)). Qed.
 End functions.
diff --git a/prelude/gmap.v b/prelude/gmap.v
index bf74baaafa5a49f93f2384d51016fa85080e2e59..1d86a695032d9cedef6e39f34260b3fc01d8da33 100644
--- a/prelude/gmap.v
+++ b/prelude/gmap.v
@@ -30,7 +30,7 @@ Proof.
 Defined.
 
 (** * Operations on the data structure *)
-Instance gmap_lookup `{Countable K} {A} : Lookup K A (gmap K A) := λ i m,
+Instance gmap_lookup `{Countable K} : Lookup K (gmap K) := λ A i m,
   let (m,_) := m in m !! encode i.
 Instance gmap_empty `{Countable K} {A} : Empty (gmap K A) := GMap ∅ I.
 Lemma gmap_partial_alter_wf `{Countable K} {A} (f : option A → option A) m i :
@@ -40,8 +40,7 @@ Proof.
   - rewrite decode_encode; eauto.
   - rewrite lookup_partial_alter_ne by done. by apply Hm.
 Qed.
-Instance gmap_partial_alter `{Countable K} {A} :
-    PartialAlter K A (gmap K A) := λ f i m,
+Instance gmap_partial_alter `{Countable K} : PartialAlter K (gmap K) := λ A f i m,
   let (m,Hm) := m in GMap (partial_alter f (encode i) m)
     (bool_decide_pack _ (gmap_partial_alter_wf f m i
     (bool_decide_unpack _ Hm))).
@@ -70,7 +69,7 @@ Instance gmap_merge `{Countable K} : Merge (gmap K) := λ A B C f m1 m2,
   let f' o1 o2 := match o1, o2 with None, None => None | _, _ => f o1 o2 end in
   GMap (merge f' m1 m2) (bool_decide_pack _ (gmap_merge_wf f _ _
     (bool_decide_unpack _ Hm1) (bool_decide_unpack _ Hm2))).
-Instance gmap_to_list `{Countable K} {A} : FinMapToList K A (gmap K A) := λ m,
+Instance gmap_to_list `{Countable K} : FinMapToList K (gmap K) := λ A m,
   let (m,_) := m in omap (λ ix : positive * A,
     let (i,x) := ix in (,x) <$> decode i) (map_to_list m).
 
@@ -114,7 +113,7 @@ Qed.
 
 (** * Finite sets *)
 Notation gset K := (mapset (gmap K)).
-Instance gset_dom `{Countable K} {A} : Dom (gmap K A) (gset K) := mapset_dom.
+Instance gset_dom `{Countable K} : Dom (gmap K) (gset K) := mapset_dom.
 Instance gset_dom_spec `{Countable K} :
   FinMapDom K (gmap K) (gset K) := mapset_dom_spec.
 
diff --git a/prelude/list.v b/prelude/list.v
index 59b26331813bf82dc7cd243e88f8721e7b9fd82e..12dc6a82ab65c58c26549c5c20eb486283e42138 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -57,15 +57,15 @@ Existing Instance list_equiv.
 
 (** The operation [l !! i] gives the [i]th element of the list [l], or [None]
 in case [i] is out of bounds. *)
-Instance list_lookup {A} : Lookup nat A (list A) :=
-  fix go i l {struct l} : option A := let _ : Lookup _ _ _ := @go in
+Instance list_lookup : Lookup nat list :=
+  fix go A i l {struct l} : option A := let _ : Lookup _ _ := @go in
   match l with
   | [] => None | x :: l => match i with 0 => Some x | S i => l !! i end
   end.
 
 (** The operation [alter f i l] applies the function [f] to the [i]th element
 of [l]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_alter {A} : Alter nat A (list A) := λ f,
+Instance list_alter : Alter nat list := λ A f,
   fix go i l {struct l} :=
   match l with
   | [] => []
@@ -74,8 +74,8 @@ Instance list_alter {A} : Alter nat A (list A) := λ f,
 
 (** The operation [<[i:=x]> l] overwrites the element at position [i] with the
 value [x]. In case [i] is out of bounds, the list is returned unchanged. *)
-Instance list_insert {A} : Insert nat A (list A) :=
-  fix go i y l {struct l} := let _ : Insert _ _ _ := @go in
+Instance list_insert : Insert nat list :=
+  fix go A i y l {struct l} := let _ : Insert _ _ := @go in
   match l with
   | [] => []
   | x :: l => match i with 0 => y :: l | S i => x :: <[i:=y]>l end
@@ -90,11 +90,11 @@ Instance: Params (@list_inserts) 1.
 (** The operation [delete i l] removes the [i]th element of [l] and moves
 all consecutive elements one position ahead. In case [i] is out of bounds,
 the list is returned unchanged. *)
-Instance list_delete {A} : Delete nat (list A) :=
-  fix go (i : nat) (l : list A) {struct l} : list A :=
+Instance list_delete : Delete nat list :=
+  fix go A (i : nat) (l : list A) {struct l} : list A :=
   match l with
   | [] => []
-  | x :: l => match i with 0 => l | S i => x :: @delete _ _ go i l end
+  | x :: l => match i with 0 => l | S i => x :: @delete _ _ go _ i l end
   end.
 
 (** The function [option_list o] converts an element [Some x] into the
@@ -2733,13 +2733,13 @@ Section setoid.
   Global Instance drop_proper n : Proper ((≡) ==> (≡)) (@drop A n).
   Proof. induction n; destruct 1; simpl; try constructor; auto. Qed.
   Global Instance list_lookup_proper i :
-    Proper ((≡) ==> (≡)) (lookup (M:=list A) i).
+    Proper ((≡) ==> (≡)) (lookup (M:=list) i).
   Proof. induction i; destruct 1; simpl; f_equiv; auto. Qed.
   Global Instance list_alter_proper f i :
-    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list A) f i).
+    Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (alter (M:=list) f i).
   Proof. intros. induction i; destruct 1; constructor; eauto. Qed.
   Global Instance list_insert_proper i :
-    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list A) i).
+    Proper ((≡) ==> (≡) ==> (≡)) (insert (M:=list) i).
   Proof. intros ???; induction i; destruct 1; constructor; eauto. Qed.
   Global Instance list_inserts_proper i :
     Proper ((≡) ==> (≡) ==> (≡)) (@list_inserts A i).
@@ -2748,7 +2748,7 @@ Section setoid.
     induction Hk; intros ????; simpl; try f_equiv; naive_solver.
   Qed.
   Global Instance list_delete_proper i :
-    Proper ((≡) ==> (≡)) (delete (M:=list A) i).
+    Proper ((≡) ==> (≡)) (delete (M:=list) i).
   Proof. induction i; destruct 1; try constructor; eauto. Qed.
   Global Instance option_list_proper : Proper ((≡) ==> (≡)) (@option_list A).
   Proof. destruct 1; by constructor. Qed.
diff --git a/prelude/mapset.v b/prelude/mapset.v
index 5a3dd7188e4f8c9f97737f0910996fe2b0bae3a1..17282118a7e9bb1a4c8e9988b6ab82eda9d903d9 100644
--- a/prelude/mapset.v
+++ b/prelude/mapset.v
@@ -118,7 +118,7 @@ Proof.
   - destruct (Is_true_reflect (f a)); naive_solver.
   - naive_solver.
 Qed.
-Instance mapset_dom {A} : Dom (M A) (mapset M) := mapset_dom_with (λ _, true).
+Instance mapset_dom : Dom M (mapset M) := λ A, mapset_dom_with (λ _, true).
 Instance mapset_dom_spec: FinMapDom K M (mapset M).
 Proof.
   split; try apply _. intros. unfold dom, mapset_dom, is_Some.
diff --git a/prelude/natmap.v b/prelude/natmap.v
index 5845901a62cf9d3fe2fc6b63806409e5c1e86b05..a79f1b982aa0609aaf274fc74819bf2fd414148f 100644
--- a/prelude/natmap.v
+++ b/prelude/natmap.v
@@ -44,7 +44,7 @@ Global Instance natmap_eq_dec `{∀ x y : A, Decision (x = y)}
   end.
 
 Instance natmap_empty {A} : Empty (natmap A) := NatMap [] I.
-Instance natmap_lookup {A} : Lookup nat A (natmap A) := λ i m,
+Instance natmap_lookup : Lookup nat natmap := λ A i m,
   let (l,_) := m in mjoin (l !! i).
 
 Fixpoint natmap_singleton_raw {A} (i : nat) (x : A) : natmap_raw A :=
@@ -92,7 +92,7 @@ Proof.
   revert i. induction l; [intro | intros [|?]]; simpl; repeat case_match;
     eauto using natmap_singleton_wf, natmap_cons_canon_wf, natmap_wf_inv.
 Qed.
-Instance natmap_alter {A} : PartialAlter nat A (natmap A) := λ f i m,
+Instance natmap_alter : PartialAlter nat natmap := λ A f i m,
   let (l,Hl) := m in NatMap _ (natmap_alter_wf f i l Hl).
 Lemma natmap_lookup_alter_raw {A} (f : option A → option A) i l :
   mjoin (natmap_alter_raw f i l !! i) = f (mjoin (l !! i)).
@@ -188,7 +188,7 @@ Proof.
   revert i. induction l as [|[?|] ? IH]; simpl; try constructor; auto.
   rewrite natmap_elem_of_to_list_raw_aux. intros (?&?&?). lia.
 Qed.
-Instance natmap_to_list {A} : FinMapToList nat A (natmap A) := λ m,
+Instance natmap_to_list : FinMapToList nat natmap := λ A m,
   let (l,_) := m in natmap_to_list_raw 0 l.
 
 Definition natmap_map_raw {A B} (f : A → B) : natmap_raw A → natmap_raw B :=
@@ -256,7 +256,7 @@ Qed.
 
 (** Finally, we can construct sets of [nat]s satisfying extensional equality. *)
 Notation natset := (mapset natmap).
-Instance natmap_dom {A} : Dom (natmap A) natset := mapset_dom.
+Instance natmap_dom : Dom natmap natset := mapset_dom.
 Instance: FinMapDom nat natmap natset := mapset_dom_spec.
 
 (* Fixpoint avoids this definition from being unfolded *)
diff --git a/prelude/nmap.v b/prelude/nmap.v
index 11fead13c53c361d4e852924c79a4aae2e08f425..c3c42ea9365310911648a9c20d453e29c98c14f4 100644
--- a/prelude/nmap.v
+++ b/prelude/nmap.v
@@ -22,17 +22,17 @@ Proof.
 Defined.
 Instance Nempty {A} : Empty (Nmap A) := NMap None ∅.
 Global Opaque Nempty.
-Instance Nlookup {A} : Lookup N A (Nmap A) := λ i t,
+Instance Nlookup : Lookup N Nmap := λ A i t,
   match i with
   | N0 => Nmap_0 t
   | Npos p => Nmap_pos t !! p
   end.
-Instance Npartial_alter {A} : PartialAlter N A (Nmap A) := λ f i t,
+Instance Npartial_alter : PartialAlter N Nmap := λ A f i t,
   match i, t with
   | N0, NMap o t => NMap (f o) t
   | Npos p, NMap o t => NMap o (partial_alter f p t)
   end.
-Instance Nto_list {A} : FinMapToList N A (Nmap A) := λ t,
+Instance Nto_list : FinMapToList N Nmap := λ A t,
   match t with
   | NMap o t =>
      default [] o (λ x, [(0,x)]) ++ (prod_map Npos id <$> map_to_list t)
@@ -82,7 +82,7 @@ Qed.
 (** * Finite sets *)
 (** We construct sets of [N]s satisfying extensional equality. *)
 Notation Nset := (mapset Nmap).
-Instance Nmap_dom {A} : Dom (Nmap A) Nset := mapset_dom.
+Instance Nmap_dom : Dom Nmap Nset := mapset_dom.
 Instance: FinMapDom N Nmap Nset := mapset_dom_spec.
 
 (** * Fresh numbers *)
diff --git a/prelude/option.v b/prelude/option.v
index 0f972ca16d9d20d29fb18feb0e59d4e0b56261b2..7c4142070e7e17ea370322163e3ab55680c6b818 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -239,16 +239,16 @@ Instance maybe_Some {A} : Maybe (@Some A) := id.
 Arguments maybe_Some _ !_ /.
 
 (** * Union, intersection and difference *)
-Instance option_union_with {A} : UnionWith A (option A) := λ f mx my,
+Instance option_union_with : UnionWith option := λ A f mx my,
   match mx, my with
   | Some x, Some y => f x y
   | Some x, None => Some x
   | None, Some y => Some y
   | None, None => None
   end.
-Instance option_intersection_with {A} : IntersectionWith A (option A) :=
-  λ f mx my, match mx, my with Some x, Some y => f x y | _, _ => None end.
-Instance option_difference_with {A} : DifferenceWith A (option A) := λ f mx my,
+Instance option_intersection_with : IntersectionWith option := λ A f mx my,
+  match mx, my with Some x, Some y => f x y | _, _ => None end.
+Instance option_difference_with : DifferenceWith option := λ A f mx my,
   match mx, my with
   | Some x, Some y => f x y
   | Some x, None => Some x
diff --git a/prelude/pmap.v b/prelude/pmap.v
index 483eac8b16690b182496e9510a4b4bb44acd2709..1416ed314887e2d741de5e841c554fb5b89b5601 100644
--- a/prelude/pmap.v
+++ b/prelude/pmap.v
@@ -52,9 +52,9 @@ Local Hint Resolve PNode_wf.
 
 (** Operations *)
 Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
-Instance Plookup_raw {A} : Lookup positive A (Pmap_raw A) :=
-  fix go (i : positive) (t : Pmap_raw A) {struct t} : option A :=
-  let _ : Lookup _ _ _ := @go in
+Instance Plookup_raw : Lookup positive Pmap_raw :=
+  fix go A (i : positive) (t : Pmap_raw A) {struct t} : option A :=
+  let _ : Lookup _ _ := @go in
   match t with
   | PLeaf => None
   | PNode o l r => match i with 1 => o | i~0 => l !! i | i~1 => r !! i end
@@ -273,12 +273,12 @@ Instance Pmap_eq_dec `{∀ x y : A, Decision (x = y)}
   | right H => right (H ∘ proj1 (Pmap_eq m1 m2))
   end.
 Instance Pempty {A} : Empty (Pmap A) := PMap ∅ I.
-Instance Plookup {A} : Lookup positive A (Pmap A) := λ i m, pmap_car m !! i.
-Instance Ppartial_alter {A} : PartialAlter positive A (Pmap A) := λ f i m,
+Instance Plookup : Lookup positive Pmap := λ A i m, pmap_car m !! i.
+Instance Ppartial_alter : PartialAlter positive Pmap := λ A f i m,
   let (t,Ht) := m in PMap (partial_alter f i t) (Ppartial_alter_wf f i _ Ht).
 Instance Pfmap : FMap Pmap := λ A B f m,
   let (t,Ht) := m in PMap (f <$> t) (Pfmap_wf f _ Ht).
-Instance Pto_list {A} : FinMapToList positive A (Pmap A) := λ m,
+Instance Pto_list : FinMapToList positive Pmap := λ A m,
   let (t,Ht) := m in Pto_list_raw 1 t [].
 Instance Pomap : OMap Pmap := λ A B f m,
   let (t,Ht) := m in PMap (omap f t) (Pomap_wf f _ Ht).
@@ -305,7 +305,7 @@ Qed.
 (** * Finite sets *)
 (** We construct sets of [positives]s satisfying extensional equality. *)
 Notation Pset := (mapset Pmap).
-Instance Pmap_dom {A} : Dom (Pmap A) Pset := mapset_dom.
+Instance Pmap_dom : Dom Pmap Pset := mapset_dom.
 Instance: FinMapDom positive Pmap Pset := mapset_dom_spec.
 
 (** * Fresh numbers *)
diff --git a/prelude/zmap.v b/prelude/zmap.v
index 238fadc46c63d485cb2a4077ff7a1acfcd34fe18..063c5b9cd149aa03457e7e2b35d9e5d440deb752 100644
--- a/prelude/zmap.v
+++ b/prelude/zmap.v
@@ -23,17 +23,17 @@ Proof.
   end; abstract congruence.
 Defined.
 Instance Zempty {A} : Empty (Zmap A) := ZMap None ∅ ∅.
-Instance Zlookup {A} : Lookup Z A (Zmap A) := λ i t,
+Instance Zlookup : Lookup Z Zmap := λ A i t,
   match i with
   | Z0 => Zmap_0 t | Zpos p => Zmap_pos t !! p | Zneg p => Zmap_neg t !! p
   end.
-Instance Zpartial_alter {A} : PartialAlter Z A (Zmap A) := λ f i t,
+Instance Zpartial_alter : PartialAlter Z Zmap := λ A f i t,
   match i, t with
   | Z0, ZMap o t t' => ZMap (f o) t t'
   | Zpos p, ZMap o t t' => ZMap o (partial_alter f p t) t'
   | Zneg p, ZMap o t t' => ZMap o t (partial_alter f p t')
   end.
-Instance Zto_list {A} : FinMapToList Z A (Zmap A) := λ t,
+Instance Zto_list : FinMapToList Z Zmap := λ A t,
   match t with
   | ZMap o t t' => default [] o (λ x, [(0,x)]) ++
      (prod_map Zpos id <$> map_to_list t) ++
@@ -93,5 +93,5 @@ Qed.
 (** * Finite sets *)
 (** We construct sets of [Z]s satisfying extensional equality. *)
 Notation Zset := (mapset Zmap).
-Instance Zmap_dom {A} : Dom (Zmap A) Zset := mapset_dom.
+Instance Zmap_dom : Dom Zmap Zset := mapset_dom.
 Instance: FinMapDom Z Zmap Zset := mapset_dom_spec.
diff --git a/program_logic/boxes.v b/program_logic/boxes.v
index e81180b7981883bb0940fa9cacbb226e59f36fc8..fd4e2cd16314789a67969a6f7f3d738af1998f81 100644
--- a/program_logic/boxes.v
+++ b/program_logic/boxes.v
@@ -102,7 +102,7 @@ Proof.
   iPvs (inv_alloc N _ (slice_inv γ Q) with "[Hγ]") as "#Hinv"; first done.
   { iNext. iExists false; eauto. }
   iPvsIntro; iExists γ; repeat iSplit; auto.
-  iNext. iExists (<[γ:=Q]> Φ); iSplit.
+  iNext. iExists (fn_insert γ Q Φ); iSplit.
   - iNext. iRewrite "HeqP". by rewrite big_sepM_fn_insert'.
   - rewrite (big_sepM_fn_insert (λ _ _ P',  _ ★ _ _ P' ★ _ _ (_ _ P')))%I //.
     iFrame; eauto.
diff --git a/program_logic/resources.v b/program_logic/resources.v
index 1590ee7374bdb68b0b5ddd2fb16d1b7f7b28f680..8795d0256384e0c5028d274eeb1b91105107424f 100644
--- a/program_logic/resources.v
+++ b/program_logic/resources.v
@@ -150,7 +150,7 @@ Lemma lookup_wld_op_l n r1 r2 i P :
   ✓{n} (r1⋅r2) → wld r1 !! i ≡{n}≡ Some P → (wld r1 ⋅ wld r2) !! i ≡{n}≡ Some P.
 Proof.
   move=>/wld_validN /(_ i) Hval Hi1P; move: Hi1P Hval; rewrite lookup_op.
-  destruct (wld r2 !! i) as [P'|] eqn:Hi; rewrite !Hi ?right_id // =>-> ?.
+  case Hi : (wld r2 !! i)=> [P'|]; rewrite ?right_id // =>-> ?.
   by constructor; rewrite (agree_op_inv _ P P') // agree_idemp.
 Qed.
 Lemma lookup_wld_op_r n r1 r2 i P :