diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 1f416c8a9b959f853ade43c8328756eedc3fbdc8..12066a20c967808f9fe003c3d7e2503ac5861ab1 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -113,7 +113,7 @@ Global Arguments gmapO _ {_ _} _.
 (** Non-expansiveness of higher-order map functions and big-ops *)
 Global Instance merge_ne `{Countable K} {A B C : ofe} n :
   Proper ((dist (A:=option A) n ==> dist (A:=option B) n ==> dist (A:=option C) n) ==>
-          dist n ==> dist n ==> dist n) (merge (MA:=gmap K A)).
+          dist n ==> dist n ==> (≡{n}@{gmap K C}≡)) merge.
 Proof.
   intros ?? Hf ?? Hm1 ?? Hm2 i. rewrite !lookup_merge.
   destruct (Hm1 i), (Hm2 i); try apply Hf; by constructor.
@@ -126,7 +126,8 @@ Proof.
   by do 2 destruct 1; first [apply Hf | constructor].
 Qed.
 Global Instance map_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (MA:=gmap K A) f).
+  Proper (dist n ==> dist n) f →
+  Proper (dist n ==> (≡{n}@{gmap K B}≡)) (fmap f).
 Proof. intros ? m m' ? k; rewrite !lookup_fmap. by repeat f_equiv. Qed.
 Global Instance map_zip_with_ne `{Countable K} {A B C : ofe} (f : A → B → C) n :
   Proper (dist n ==> dist n ==> dist n) f →
@@ -713,9 +714,6 @@ Qed.
 End unital_properties.
 
 (** Functor *)
-Global Instance gmap_fmap_ne `{Countable K} {A B : ofe} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (MA:=gmap K A) f).
-Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
 Lemma gmap_fmap_ne_ext `{Countable K}
   {A : Type} {B : ofe} (f1 f2 : A → B) (m : gmap K A) n :
   (∀ i x, m !! i = Some x → f1 x ≡{n}≡ f2 x) →
diff --git a/iris/algebra/list.v b/iris/algebra/list.v
index 3327138d89e9a069e646015c90566336dca39d1d..3c64afd659e110a91097ab9179cbae087dffa882 100644
--- a/iris/algebra/list.v
+++ b/iris/algebra/list.v
@@ -125,10 +125,10 @@ Global Arguments listO : clear implicits.
 
 (** Non-expansiveness of higher-order list functions and big-ops *)
 Global Instance list_fmap_ne {A B : ofe} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (fmap (MA:=list A) (MB:=list B)).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list A}≡) ==> (≡{n}@{list B}≡)) fmap.
 Proof. intros f1 f2 Hf l1 l2 Hl; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Global Instance list_omap_ne {A B : ofe} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (omap (MA:=list A) (MB:=list B)).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list A}≡) ==> (≡{n}@{list B}≡)) omap.
 Proof.
   intros f1 f2 Hf. induction 1 as [|x1 x2 l1 l2 Hx Hl]; csimpl; [constructor|].
   destruct (Hf _ _ Hx); [f_equiv|]; auto.
@@ -142,10 +142,10 @@ Proof.
   f_equiv; [by apply Hf|]. apply IH. intros i y1 y2 Hy. by apply Hf.
 Qed.
 Global Instance list_bind_ne {A B : ofe} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n)
-         (mbind (A:=A) (MA:=list A) (MB:=list B)).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{list B}≡) ==> (≡{n}@{list A}≡)) mbind.
 Proof. intros f1 f2 Hf. induction 1; csimpl; [constructor|f_equiv; auto]. Qed.
-Global Instance list_join_ne {A : ofe} : NonExpansive (mjoin (MA:=list A)).
+Global Instance list_join_ne {A : ofe} n :
+  Proper (dist n ==> (≡{n}@{list A}≡)) mjoin.
 Proof. induction 1; simpl; [constructor|solve_proper]. Qed.
 Global Instance zip_with_ne {A B C : ofe} n :
   Proper ((dist n ==> dist n ==> dist n) ==> dist n ==> dist n ==> dist n)
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 002c881ee837fc1cbb580ded5597bee3a720a30e..318577d095d5bfa1a2bf89b93c664485b89d54ba 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1295,13 +1295,13 @@ Global Typeclasses Opaque option_dist.
 Global Arguments optionO : clear implicits.
 
 Global Instance option_fmap_ne {A B : ofe} n:
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap A B (option A) (option B) _).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{option A}≡) ==> (≡{n}@{option B}≡)) fmap.
 Proof. intros f f' Hf ?? []; constructor; auto. Qed.
 Global Instance option_mbind_ne {A B : ofe} n:
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@mbind A (option A) (option B) _).
+  Proper ((dist n ==> dist n) ==> (≡{n}@{option A}≡) ==> (≡{n}@{option B}≡)) mbind.
 Proof. destruct 2; simpl; auto. Qed.
 Global Instance option_mjoin_ne {A : ofe} n:
-  Proper (dist n ==> dist n) (@mjoin (option A) (option (option A)) _).
+  Proper (dist n ==> (≡{n}@{option A}≡)) mjoin.
 Proof. destruct 1 as [?? []|]; simpl; by constructor. Qed.
 
 Global Instance option_fmap_dist_inj {A B : ofe} (f : A → B) n :
diff --git a/iris_unstable/heap_lang/interpreter.v b/iris_unstable/heap_lang/interpreter.v
index 05c597ff52f4027d5a0bc04a5074174ccae94436..3f39a044a3eaa848f34a1c7b668ba5ad67af4a65 100644
--- a/iris_unstable/heap_lang/interpreter.v
+++ b/iris_unstable/heap_lang/interpreter.v
@@ -151,7 +151,7 @@ Module interp_monad.
   Proof. by inversion 1. Qed.
 
   Lemma mret_inv {A} (v: A) s v' s' :
-    mret (MA:=InterpretM A) v s = (inl v', s') → v = v' ∧ s = s'.
+    (mret v : InterpretM A) s = (inl v', s') → v = v' ∧ s = s'.
   Proof. by inversion 1. Qed.
 
   Lemma interp_bind_inv A B (x: InterpretM A) (f: A → InterpretM B) r s s' :
@@ -176,7 +176,7 @@ Module interp_monad.
   Qed.
 
   Lemma interp_fmap_inv {A B} (f: A → B) x s v s' :
-    (fmap (MA:=InterpretM A) f x) s = (inl v, s') →
+    (fmap f x : InterpretM B) s = (inl v, s') →
     ∃ v0, v = f v0 ∧ x s = (inl v0, s').
   Proof.
     rewrite /fmap /interp_fmap.
@@ -240,7 +240,7 @@ Module interp_monad.
   Qed.
 
   Lemma interp_fmap_inr_inv {A B} (f: A → B) (x: InterpretM A) s e s' :
-    (fmap (MB := InterpretM B) f x) s = (inr e, s') →
+    (fmap f x : InterpretM B) s = (inr e, s') →
     x s = (inr e, s').
   Proof.
     rewrite /fmap /interp_fmap.
diff --git a/tests/algebra.v b/tests/algebra.v
index 082f6e9e7fe8974f1034fb43781198896d4ddc52..f0aad6dfa5401e8b759dce59740128961bc3db44 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -92,5 +92,5 @@ Proof. apply _. Qed.
 
 (** Regression test for https://gitlab.mpi-sws.org/iris/iris/-/issues/577 *)
 Lemma list_bind_ne_test {A B : ofe} (f : A → list B) :
-  NonExpansive f → NonExpansive (mbind (MA:=list A) f).
+  NonExpansive f → NonExpansive (mbind f : list A → list B).
 Proof. apply _. Qed.