diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 1c131d41814da0b946ccfd812746d0ff14950d7f..df78c64fe5be742685e05a5dc1dd4fe6858f8d46 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -28,6 +28,10 @@ Global Hint Extern 0 (_ ≡{_}≡ _) => reflexivity : core.
 Global Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption : core.
 Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
 Notation NonExpansive2 f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).
+Notation NonExpansive3 f :=
+  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) f).
+Notation NonExpansive4 f :=
+  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f).
 
 Tactic Notation "ofe_subst" ident(x) :=
   repeat match goal with
@@ -614,9 +618,9 @@ Proof. apply ne_proper_2; apply _. Qed.
 (* Function space maps *)
 Definition ofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
   (h : A -n> B) : A' -n> B' := g â—Ž h â—Ž f.
-Global Instance ofe_mor_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n ==> dist n) (@ofe_mor_map A A' B B').
-Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
+Global Instance ofe_mor_map_ne {A A' B B'} :
+  NonExpansive3 (@ofe_mor_map A A' B B').
+Proof. intros n ??? ??? ???. by repeat apply ccompose_ne. Qed.
 
 Definition ofe_morO_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
   (A -n> B) -n> (A' -n>  B') := OfeMor (ofe_mor_map f g).
diff --git a/tests/algebra.v b/tests/algebra.v
index 23edb90385383d86bb4c4d522c4ee4a836b00c6c..e62e613f8c194a63ad547d9515250636fd0c50bb 100644
--- a/tests/algebra.v
+++ b/tests/algebra.v
@@ -70,27 +70,21 @@ Definition gmap_view_check {K : Type} `{Countable K} {V : ofe} :
   gmap_view K V = gmap_viewO K V := eq_refl.
 
 Lemma uncurry_ne_test {A B C : ofe} (f : A → B → C) :
-  (∀ n, Proper (dist n ==> dist n ==> dist n) f) →
-  NonExpansive (uncurry f).
+  NonExpansive2 f → NonExpansive (uncurry f).
 Proof. apply _. Qed.
 Lemma uncurry3_ne_test {A B C D : ofe} (f : A → B → C → D) :
-  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) f) →
-  NonExpansive (uncurry3 f).
+  NonExpansive3 f → NonExpansive (uncurry3 f).
 Proof. apply _. Qed.
 Lemma uncurry4_ne_test {A B C D E : ofe} (f : A → B → C → D → E) :
-  (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f) →
-  NonExpansive (uncurry4 f).
+  NonExpansive4 f → NonExpansive (uncurry4 f).
 Proof. apply _. Qed.
 
 Lemma curry_ne_test {A B C : ofe} (f : A * B → C) :
-  NonExpansive f →
-  ∀ n, Proper (dist n ==> dist n ==> dist n) (curry f).
+  NonExpansive f → NonExpansive2 (curry f).
 Proof. apply _. Qed.
 Lemma curry3_ne_test {A B C D : ofe} (f : A * B * C → D) :
-  NonExpansive f →
-  ∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) (curry3 f).
+  NonExpansive f → NonExpansive3 (curry3 f).
 Proof. apply _. Qed.
 Lemma curry4_ne_test {A B C D E : ofe} (f : A * B * C * D → E) :
-  NonExpansive f →
-  ∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) (curry4 f).
+  NonExpansive f → NonExpansive4 (curry4 f).
 Proof. apply _. Qed.