diff --git a/theories/algebra/agree.v b/theories/algebra/agree.v
index dca816351f3e94eee115f8612ed420a60898d7af..6dbb677f2213370298615c3f5885570fd3fb4db9 100644
--- a/theories/algebra/agree.v
+++ b/theories/algebra/agree.v
@@ -271,12 +271,12 @@ Proof.
   split; rewrite Hxy; done.
 Qed.
 
-Instance: ∀ x : agree A, Proper (dist n ==> dist n) (op x).
+Instance: ∀ x : agree A, NonExpansive (op x).
 Proof.
-  intros n x y1 y2. rewrite /dist /agree_dist /agree_list /=. 
+  intros x n y1 y2. rewrite /dist /agree_dist /agree_list /=. 
   rewrite !app_comm_cons. apply: list_setequiv_app.
 Qed.
-Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
+Instance: NonExpansive2 (@op (agree A) _).
 Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
 Instance: Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
 Instance: Assoc (≡) (@op (agree A) _).
@@ -347,7 +347,7 @@ Qed.
 Definition to_agree (x : A) : agree A :=
   {| agree_car := x; agree_with := [] |}.
 
-Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
+Global Instance to_agree_ne : NonExpansive to_agree.
 Proof.
   intros x1 x2 Hx; rewrite /= /dist /agree_dist /=.
   exact: list_setequiv_singleton.
@@ -420,11 +420,11 @@ Lemma agree_map_compose {A B C} (f : A → B) (g : B → C) (x : agree A) :
 Proof. rewrite /agree_map /= list_fmap_compose. done. Qed.
 
 Section agree_map.
-  Context {A B : ofeT} (f : A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
+  Context {A B : ofeT} (f : A → B) `{Hf: NonExpansive f}.
   Collection Hyps := Type Hf.
-  Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
+  Instance agree_map_ne : NonExpansive (agree_map f).
   Proof using Hyps.
-    intros x y Hxy.
+    intros n x y Hxy.
     change (list_setequiv (dist n)(f <$> (agree_list x))(f <$> (agree_list y))).
     eapply list_setequiv_fmap; last exact Hxy. apply _. 
   Qed.
@@ -452,9 +452,9 @@ End agree_map.
 
 Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
   CofeMor (agree_map f : agreeC A → agreeC B).
-Instance agreeC_map_ne A B n : Proper (dist n ==> dist n) (@agreeC_map A B).
+Instance agreeC_map_ne A B : NonExpansive (@agreeC_map A B).
 Proof.
-  intros f g Hfg x. apply: list_setequiv_ext.
+  intros n f g Hfg x. apply: list_setequiv_ext.
   change (f <$> (agree_list x) ≡{n}≡ g <$> (agree_list x)).
   apply list_fmap_ext_ne. done.
 Qed.
diff --git a/theories/algebra/auth.v b/theories/algebra/auth.v
index 25b17ea48256aa2376433d2bd55d3349c6af07de..5a976d77da10a6b38f73c973f471a99220ea73eb 100644
--- a/theories/algebra/auth.v
+++ b/theories/algebra/auth.v
@@ -23,15 +23,15 @@ Instance auth_equiv : Equiv (auth A) := λ x y,
 Instance auth_dist : Dist (auth A) := λ n x y,
   authoritative x ≡{n}≡ authoritative y ∧ auth_own x ≡{n}≡ auth_own y.
 
-Global Instance Auth_ne : Proper (dist n ==> dist n ==> dist n) (@Auth A).
+Global Instance Auth_ne : NonExpansive2 (@Auth A).
 Proof. by split. Qed.
 Global Instance Auth_proper : Proper ((≡) ==> (≡) ==> (≡)) (@Auth A).
 Proof. by split. Qed.
-Global Instance authoritative_ne: Proper (dist n ==> dist n) (@authoritative A).
+Global Instance authoritative_ne: NonExpansive (@authoritative A).
 Proof. by destruct 1. Qed.
 Global Instance authoritative_proper : Proper ((≡) ==> (≡)) (@authoritative A).
 Proof. by destruct 1. Qed.
-Global Instance own_ne : Proper (dist n ==> dist n) (@auth_own A).
+Global Instance own_ne : NonExpansive (@auth_own A).
 Proof. by destruct 1. Qed.
 Global Instance own_proper : Proper ((≡) ==> (≡)) (@auth_own A).
 Proof. by destruct 1. Qed.
@@ -295,8 +295,8 @@ Proof.
 Qed.
 Definition authC_map {A B} (f : A -n> B) : authC A -n> authC B :=
   CofeMor (auth_map f).
-Lemma authC_map_ne A B n : Proper (dist n ==> dist n) (@authC_map A B).
-Proof. intros f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
+Lemma authC_map_ne A B : NonExpansive (@authC_map A B).
+Proof. intros n f f' Hf [[[a|]|] b]; repeat constructor; apply Hf. Qed.
 
 Program Definition authRF (F : urFunctor) : rFunctor := {|
   rFunctor_car A B := authR (urFunctor_car F A B);
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3a1b8aaff9872d03db666b0c55ebcba5917ee9cb..0db38d070637d9c4a92531a309208afc1931eb7e 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -37,7 +37,7 @@ Hint Extern 0 (_ ≼{_} _) => reflexivity.
 
 Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
   (* setoids *)
-  mixin_cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x);
+  mixin_cmra_op_ne (x : A) : NonExpansive (op x);
   mixin_cmra_pcore_ne n x y cx :
     x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
   mixin_cmra_validN_ne n : Proper (dist n ==> impl) (validN n);
@@ -93,7 +93,7 @@ Canonical Structure cmra_ofeC.
 Section cmra_mixin.
   Context {A : cmraT}.
   Implicit Types x y : A.
-  Global Instance cmra_op_ne n (x : A) : Proper (dist n ==> dist n) (op x).
+  Global Instance cmra_op_ne (x : A) : NonExpansive (op x).
   Proof. apply (mixin_cmra_op_ne _ (cmra_mixin A)). Qed.
   Lemma cmra_pcore_ne n x y cx :
     x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy.
@@ -211,7 +211,7 @@ Class CMRADiscrete (A : cmraT) := {
 
 (** * Morphisms *)
 Class CMRAMonotone {A B : cmraT} (f : A → B) := {
-  cmra_monotone_ne n :> Proper (dist n ==> dist n) f;
+  cmra_monotone_ne :> NonExpansive f;
   cmra_monotone_validN n x : ✓{n} x → ✓{n} f x;
   cmra_monotone x y : x ≼ y → f x ≼ f y
 }.
@@ -221,7 +221,7 @@ Arguments cmra_monotone {_ _} _ {_} _ _ _.
 (* Not all intended homomorphisms preserve validity, in particular it does not
 hold for the [ownM] and [own] connectives. *)
 Class CMRAHomomorphism {A B : cmraT} (f : A → B) := {
-  cmra_homomorphism_ne n :> Proper (dist n ==> dist n) f;
+  cmra_homomorphism_ne :> NonExpansive f;
   cmra_homomorphism x y : f (x ⋅ y) ≡ f x ⋅ f y
 }.
 Arguments cmra_homomorphism {_ _} _ _ _ _.
@@ -239,9 +239,9 @@ Implicit Types x y z : A.
 Implicit Types xs ys zs : list A.
 
 (** ** Setoids *)
-Global Instance cmra_pcore_ne' n : Proper (dist n ==> dist n) (@pcore A _).
+Global Instance cmra_pcore_ne' : NonExpansive (@pcore A _).
 Proof.
-  intros x y Hxy. destruct (pcore x) as [cx|] eqn:?.
+  intros n x y Hxy. destruct (pcore x) as [cx|] eqn:?.
   { destruct (cmra_pcore_ne n x y cx) as (cy&->&->); auto. }
   destruct (pcore y) as [cy|] eqn:?; auto.
   destruct (cmra_pcore_ne n y x cy) as (cx&?&->); simplify_eq/=; auto.
@@ -255,8 +255,8 @@ Proof.
 Qed.
 Global Instance cmra_pcore_proper' : Proper ((≡) ==> (≡)) (@pcore A _).
 Proof. apply (ne_proper _). Qed.
-Global Instance cmra_op_ne' n : Proper (dist n ==> dist n ==> dist n) (@op A _).
-Proof. intros x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
+Global Instance cmra_op_ne' : NonExpansive2 (@op A _).
+Proof. intros n x1 x2 Hx y1 y2 Hy. by rewrite Hy (comm _ x1) Hx (comm _ y2). Qed.
 Global Instance cmra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
 Proof. apply (ne_proper_2 _). Qed.
 Global Instance cmra_validN_ne' : Proper (dist n ==> iff) (@validN A _ n) | 1.
@@ -287,7 +287,7 @@ Proof.
   intros x x' Hx y y' Hy.
   by split; intros [z ?]; exists z; [rewrite -Hx -Hy|rewrite Hx Hy].
 Qed.
-Global Instance cmra_opM_ne n : Proper (dist n ==> dist n ==> dist n) (@opM A).
+Global Instance cmra_opM_ne : NonExpansive2 (@opM A).
 Proof. destruct 2; by cofe_subst. Qed.
 Global Instance cmra_opM_proper : Proper ((≡) ==> (≡) ==> (≡)) (@opM A).
 Proof. destruct 2; by setoid_subst. Qed.
@@ -448,9 +448,9 @@ Section total_core.
     by rewrite /core /= Hcx Hcy.
   Qed.
 
-  Global Instance cmra_core_ne n : Proper (dist n ==> dist n) (@core A _).
+  Global Instance cmra_core_ne : NonExpansive (@core A _).
   Proof.
-    intros x y Hxy. destruct (cmra_total x) as [cx Hcx].
+    intros n x y Hxy. destruct (cmra_total x) as [cx Hcx].
     by rewrite /core /= -Hxy Hcx.
   Qed.
   Global Instance cmra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
@@ -616,8 +616,8 @@ End ucmra_leibniz.
 Section cmra_total.
   Context A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A}.
   Context (total : ∀ x, is_Some (pcore x)).
-  Context (op_ne : ∀ n (x : A), Proper (dist n ==> dist n) (op x)).
-  Context (core_ne : ∀ n, Proper (dist n ==> dist n) (@core A _)).
+  Context (op_ne : ∀ (x : A), NonExpansive (op x)).
+  Context (core_ne : NonExpansive (@core A _)).
   Context (validN_ne : ∀ n, Proper (dist n ==> impl) (@validN A _ n)).
   Context (valid_validN : ∀ (x : A), ✓ x ↔ ∀ n, ✓{n} x).
   Context (validN_S : ∀ n (x : A), ✓{S n} x → ✓{n} x).
@@ -693,8 +693,8 @@ Structure rFunctor := RFunctor {
   rFunctor_car : ofeT → ofeT → cmraT;
   rFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → rFunctor_car A1 B1 -n> rFunctor_car A2 B2;
-  rFunctor_ne A1 A2 B1 B2 n :
-    Proper (dist n ==> dist n) (@rFunctor_map A1 A2 B1 B2);
+  rFunctor_ne A1 A2 B1 B2 :
+    NonExpansive (@rFunctor_map A1 A2 B1 B2);
   rFunctor_id {A B} (x : rFunctor_car A B) : rFunctor_map (cid,cid) x ≡ x;
   rFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
@@ -726,8 +726,8 @@ Structure urFunctor := URFunctor {
   urFunctor_car : ofeT → ofeT → ucmraT;
   urFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → urFunctor_car A1 B1 -n> urFunctor_car A2 B2;
-  urFunctor_ne A1 A2 B1 B2 n :
-    Proper (dist n ==> dist n) (@urFunctor_map A1 A2 B1 B2);
+  urFunctor_ne A1 A2 B1 B2 :
+    NonExpansive (@urFunctor_map A1 A2 B1 B2);
   urFunctor_id {A B} (x : urFunctor_car A B) : urFunctor_map (cid,cid) x ≡ x;
   urFunctor_compose {A1 A2 A3 B1 B2 B3}
       (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
@@ -762,7 +762,7 @@ Definition cmra_transport {A B : cmraT} (H : A = B) (x : A) : B :=
 Section cmra_transport.
   Context {A B : cmraT} (H : A = B).
   Notation T := (cmra_transport H).
-  Global Instance cmra_transport_ne n : Proper (dist n ==> dist n) T.
+  Global Instance cmra_transport_ne : NonExpansive T.
   Proof. by intros ???; destruct H. Qed.
   Global Instance cmra_transport_proper : Proper ((≡) ==> (≡)) T.
   Proof. by intros ???; destruct H. Qed.
@@ -1178,7 +1178,7 @@ Section option.
   Proof.
     apply cmra_total_mixin.
     - eauto.
-    - by intros n [x|]; destruct 1; constructor; cofe_subst.
+    - by intros [x|] n; destruct 1; constructor; cofe_subst.
     - destruct 1; by cofe_subst.
     - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
     - intros [x|]; [apply cmra_valid_validN|done].
diff --git a/theories/algebra/cmra_big_op.v b/theories/algebra/cmra_big_op.v
index f66dcdbcc2cf698cc8c5306b5476e12b0cc18e36..b7a1c390a3a661b5d1dfb5f161e05a47dacb21ef 100644
--- a/theories/algebra/cmra_big_op.v
+++ b/theories/algebra/cmra_big_op.v
@@ -76,8 +76,8 @@ Lemma big_op_Forall2 R :
   Proper (Forall2 R ==> R) (@big_op M).
 Proof. rewrite /Proper /respectful. induction 3; eauto. Qed.
 
-Global Instance big_op_ne n : Proper (dist n ==> dist n) (@big_op M).
-Proof. apply big_op_Forall2; apply _. Qed.
+Global Instance big_op_ne : NonExpansive (@big_op M).
+Proof. intros ?. apply big_op_Forall2; apply _. Qed.
 Global Instance big_op_proper : Proper ((≡) ==> (≡)) (@big_op M) := ne_proper _.
 
 Lemma big_op_nil : [⋅] (@nil M) = ∅.
diff --git a/theories/algebra/cofe_solver.v b/theories/algebra/cofe_solver.v
index d7823128b15669c07a73bc2120f5eb256906e9d2..0474eb3a8b2d9fdb32cb6695c2190976b04b3c0e 100644
--- a/theories/algebra/cofe_solver.v
+++ b/theories/algebra/cofe_solver.v
@@ -98,7 +98,7 @@ Qed.
 Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
 Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower IH]. Qed.
 
-Instance tower_car_ne n k : Proper (dist n ==> dist n) (λ X, tower_car X k).
+Instance tower_car_ne k : NonExpansive (λ X, tower_car X k).
 Proof. by intros X Y HX. Qed.
 Definition project (k : nat) : T -n> A k := CofeMor (λ X : T, tower_car X k).
 
@@ -152,8 +152,8 @@ Program Definition embed (k : nat) (x : A k) : T :=
   {| tower_car n := embed_coerce n x |}.
 Next Obligation. intros k x i. apply g_embed_coerce. Qed.
 Instance: Params (@embed) 1.
-Instance embed_ne k n : Proper (dist n ==> dist n) (embed k).
-Proof. by intros x y Hxy i; rewrite /= Hxy. Qed.
+Instance embed_ne k : NonExpansive (embed k).
+Proof. by intros n x y Hxy i; rewrite /= Hxy. Qed.
 Definition embed' (k : nat) : A k -n> T := CofeMor (embed k).
 Lemma embed_f k (x : A k) : embed (S k) (f k x) ≡ embed k x.
 Proof.
@@ -188,7 +188,7 @@ Next Obligation.
   by apply (contractive_ne map); split=> Y /=; rewrite ?g_tower ?embed_f.
 Qed.
 Definition unfold (X : T) : F T := compl (unfold_chain X).
-Instance unfold_ne : Proper (dist n ==> dist n) unfold.
+Instance unfold_ne : NonExpansive unfold.
 Proof.
   intros n X Y HXY. by rewrite /unfold (conv_compl n (unfold_chain X))
     (conv_compl n (unfold_chain Y)) /= (HXY (S n)).
@@ -201,7 +201,7 @@ Next Obligation.
   rewrite g_S -cFunctor_compose.
   apply (contractive_proper map); split=> Y; [apply embed_f|apply g_tower].
 Qed.
-Instance fold_ne : Proper (dist n ==> dist n) fold.
+Instance fold_ne : NonExpansive fold.
 Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
 
 Theorem result : solution F.
diff --git a/theories/algebra/csum.v b/theories/algebra/csum.v
index 84181b21c8b117e52771104d7a6ff12c6c978f0d..a2a508433c76402fae42340957a41d29cfcbd5a7 100644
--- a/theories/algebra/csum.v
+++ b/theories/algebra/csum.v
@@ -39,7 +39,7 @@ Inductive csum_dist : Dist (csum A B) :=
   | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
 Existing Instance csum_dist.
 
-Global Instance Cinl_ne n : Proper (dist n ==> dist n) (@Cinl A B).
+Global Instance Cinl_ne : NonExpansive (@Cinl A B).
 Proof. by constructor. Qed.
 Global Instance Cinl_proper : Proper ((≡) ==> (≡)) (@Cinl A B).
 Proof. by constructor. Qed.
@@ -47,7 +47,7 @@ Global Instance Cinl_inj : Inj (≡) (≡) (@Cinl A B).
 Proof. by inversion_clear 1. Qed.
 Global Instance Cinl_inj_dist n : Inj (dist n) (dist n) (@Cinl A B).
 Proof. by inversion_clear 1. Qed.
-Global Instance Cinr_ne n : Proper (dist n ==> dist n) (@Cinr A B).
+Global Instance Cinr_ne : NonExpansive (@Cinr A B).
 Proof. by constructor. Qed.
 Global Instance Cinr_proper : Proper ((≡) ==> (≡)) (@Cinr A B).
 Proof. by constructor. Qed.
@@ -132,9 +132,9 @@ Proof. intros f f' Hf g g' Hg []; destruct 1; constructor; by apply Hf || apply
 Definition csumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
   csumC A B -n> csumC A' B' :=
   CofeMor (csum_map f g).
-Instance csumC_map_ne A A' B B' n :
-  Proper (dist n ==> dist n ==> dist n) (@csumC_map A A' B B').
-Proof. by intros f f' Hf g g' Hg []; constructor. Qed.
+Instance csumC_map_ne A A' B B' :
+  NonExpansive2 (@csumC_map A A' B B').
+Proof. by intros n f f' Hf g g' Hg []; constructor. Qed.
 
 Section cmra.
 Context {A B : cmraT}.
@@ -189,7 +189,7 @@ Qed.
 Lemma csum_cmra_mixin : CMRAMixin (csum A B).
 Proof.
   split.
-  - intros n []; destruct 1; constructor; by cofe_subst.
+  - intros [] n; destruct 1; constructor; by cofe_subst.
   - intros ???? [n a a' Ha|n b b' Hb|n] [=]; subst; eauto.
     + destruct (pcore a) as [ca|] eqn:?; simplify_option_eq.
       destruct (cmra_pcore_ne n a a' ca) as (ca'&->&?); auto.
diff --git a/theories/algebra/excl.v b/theories/algebra/excl.v
index d1ebb4648a4e3c75786edbc7d369902a853a3dd2..ca8757a07cfae769bd8e771d9c1c3c1fd3e10a81 100644
--- a/theories/algebra/excl.v
+++ b/theories/algebra/excl.v
@@ -32,7 +32,7 @@ Inductive excl_dist : Dist (excl A) :=
   | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
 Existing Instance excl_dist.
 
-Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
+Global Instance Excl_ne : NonExpansive (@Excl A).
 Proof. by constructor. Qed.
 Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
 Proof. by constructor. Qed.
@@ -152,7 +152,7 @@ Instance excl_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
 Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
 Instance excl_map_cmra_monotone {A B : ofeT} (f : A → B) :
-  (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
+  NonExpansive f → CMRAMonotone (excl_map f).
 Proof.
   split; try apply _.
   - by intros n [a|].
@@ -161,8 +161,8 @@ Proof.
 Qed.
 Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
   CofeMor (excl_map f).
-Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
-Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
+Instance exclC_map_ne A B : NonExpansive (@exclC_map A B).
+Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
 
 Program Definition exclRF (F : cFunctor) : rFunctor := {|
   rFunctor_car A B := (exclR (cFunctor_car F A B));
diff --git a/theories/algebra/gmap.v b/theories/algebra/gmap.v
index a239fd22c6dceae1eac612429e9884a7891de771..bf43c466609794f2b6fe1f73809aa27f3cb51c23 100644
--- a/theories/algebra/gmap.v
+++ b/theories/algebra/gmap.v
@@ -43,8 +43,8 @@ Proof. intros ? m m' ? i. by apply (timeless _). Qed.
 Global Instance gmapC_leibniz: LeibnizEquiv A → LeibnizEquiv gmapC.
 Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
 
-Global Instance lookup_ne n k :
-  Proper (dist n ==> dist n) (lookup k : gmap K A → option A).
+Global Instance lookup_ne k :
+  NonExpansive (lookup k : gmap K A → option A).
 Proof. by intros m1 m2. Qed.
 Global Instance lookup_proper k :
   Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
@@ -54,19 +54,19 @@ Proof.
   intros ? m m' Hm k'.
   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).
+Global Instance insert_ne i :
+  NonExpansive2 (insert (M:=gmap K A) i).
 Proof.
-  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
+  intros n x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
     [by constructor|by apply lookup_ne].
 Qed.
-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).
+Global Instance singleton_ne i :
+  NonExpansive (singletonM i : A → gmap K A).
+Proof. by intros ????; apply insert_ne. Qed.
+Global Instance delete_ne i :
+  NonExpansive (delete (M:=gmap K A) i).
 Proof.
-  intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
+  intros n m m' ? j; destruct (decide (i = j)); simplify_map_eq;
     [by constructor|by apply lookup_ne].
 Qed.
 
@@ -460,10 +460,10 @@ Proof.
 Qed.
 Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
   gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A → gmapC K B).
-Instance gmapC_map_ne `{Countable K} {A B} n :
-  Proper (dist n ==> dist n) (@gmapC_map K _ _ A B).
+Instance gmapC_map_ne `{Countable K} {A B} :
+  NonExpansive (@gmapC_map K _ _ A B).
 Proof.
-  intros f g Hf m k; rewrite /= !lookup_fmap.
+  intros n f g Hf m k; rewrite /= !lookup_fmap.
   destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
 Qed.
 
diff --git a/theories/algebra/iprod.v b/theories/algebra/iprod.v
index 581c7207f4444a1ce0233b3a66fb2a734f35e971..6077ee0fe18f69b9dfdfe78e077e444707d2d6f5 100644
--- a/theories/algebra/iprod.v
+++ b/theories/algebra/iprod.v
@@ -43,10 +43,10 @@ Section iprod_cofe.
   Qed.
 
   (** Properties of iprod_insert. *)
-  Global Instance iprod_insert_ne n x :
-    Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
+  Global Instance iprod_insert_ne x :
+    NonExpansive2 (iprod_insert x).
   Proof.
-    intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
+    intros n y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
     by destruct (decide _) as [[]|].
   Qed.
   Global Instance iprod_insert_proper x :
@@ -188,9 +188,9 @@ Section iprod_singleton.
   Context `{Finite A} {B : A → ucmraT}.
   Implicit Types x : A.
 
-  Global Instance iprod_singleton_ne n x :
-    Proper (dist n ==> dist n) (iprod_singleton x : B x → _).
-  Proof. intros y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
+  Global Instance iprod_singleton_ne x :
+    NonExpansive (iprod_singleton x : B x → _).
+  Proof. intros n y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
   Global Instance iprod_singleton_proper x :
     Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
 
@@ -297,9 +297,9 @@ Qed.
 Definition iprodC_map `{Finite A} {B1 B2 : A → ofeT}
     (f : iprod (λ x, B1 x -n> B2 x)) :
   iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne `{Finite A} {B1 B2 : A → ofeT} n :
-  Proper (dist n ==> dist n) (@iprodC_map A _ _ B1 B2).
-Proof. intros f1 f2 Hf g x; apply Hf. Qed.
+Instance iprodC_map_ne `{Finite A} {B1 B2 : A → ofeT} :
+  NonExpansive (@iprodC_map A _ _ B1 B2).
+Proof. intros n f1 f2 Hf g x; apply Hf. Qed.
 
 Program Definition iprodCF `{Finite C} (F : C → cFunctor) : cFunctor := {|
   cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
diff --git a/theories/algebra/list.v b/theories/algebra/list.v
index e2049d9bf98000326c8d32404010facbf05e384e..d4b01fa6712ffcdc2feada8e4a8d2b2ee6a904ad 100644
--- a/theories/algebra/list.v
+++ b/theories/algebra/list.v
@@ -12,36 +12,36 @@ Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
 Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
 Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.
 
-Global Instance cons_ne n : Proper (dist n ==> dist n ==> dist n) (@cons A) := _.
-Global Instance app_ne n : Proper (dist n ==> dist n ==> dist n) (@app A) := _.
+Global Instance cons_ne : NonExpansive2 (@cons A) := _.
+Global Instance app_ne : NonExpansive2 (@app A) := _.
 Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
-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).
-Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
+Global Instance tail_ne : NonExpansive (@tail A) := _.
+Global Instance take_ne : NonExpansive (@take A n) := _.
+Global Instance drop_ne : NonExpansive (@drop A n) := _.
+Global Instance list_lookup_ne i :
+  NonExpansive (lookup (M:=list A) 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) := _.
-Global Instance list_insert_ne n i :
-  Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) 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) := _.
-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_insert_ne i :
+  NonExpansive2 (insert (M:=list A) i) := _.
+Global Instance list_inserts_ne i :
+  NonExpansive2 (@list_inserts A i) := _.
+Global Instance list_delete_ne i :
+  NonExpansive (delete (M:=list A) i) := _.
+Global Instance option_list_ne : NonExpansive (@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)} :
   Proper (dist n ==> iff) P →
   Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
-Global Instance replicate_ne n :
-  Proper (dist n ==> dist n) (@replicate A n) := _.
-Global Instance reverse_ne n : Proper (dist n ==> dist n) (@reverse A) := _.
-Global Instance last_ne n : Proper (dist n ==> dist n) (@last A).
-Proof. intros ???; by apply dist_option_Forall2, Forall2_last. Qed.
+Global Instance replicate_ne :
+  NonExpansive (@replicate A n) := _.
+Global Instance reverse_ne : NonExpansive (@reverse A) := _.
+Global Instance last_ne : NonExpansive (@last A).
+Proof. intros ????; by apply dist_option_Forall2, Forall2_last. Qed.
 Global Instance resize_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@resize A n) := _.
+  NonExpansive2 (@resize A n) := _.
 
 Definition list_ofe_mixin : OfeMixin (list A).
 Proof.
@@ -97,8 +97,8 @@ Instance list_fmap_ne {A B : ofeT} (f : A → B) n:
 Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
 Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
   CofeMor (fmap f : listC A → listC B).
-Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
-Proof. intros f g ? l. by apply list_fmap_ext_ne. Qed.
+Instance listC_map_ne A B : NonExpansive (@listC_map A B).
+Proof. intros n f g ? l. by apply list_fmap_ext_ne. Qed.
 
 Program Definition listCF (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := listC (cFunctor_car F A B);
@@ -293,9 +293,9 @@ 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).
-  Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
+  Global Instance list_singletonM_ne i :
+    NonExpansive (@list_singletonM A i).
+  Proof. intros n l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
   Global Instance list_singletonM_proper i :
     Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
 
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 28ecdb3a4219ff5cd458ba0b666bb97fc980dc28..d3ebd8e71cb0cbf2877b6a719a1f05fb868a652f 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -17,6 +17,8 @@ Notation "x ≡{ n }≡ y" := (dist n x y)
   (at level 70, n at next level, format "x  ≡{ n }≡  y").
 Hint Extern 0 (_ ≡{_}≡ _) => reflexivity.
 Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption.
+Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
+Notation NonExpansive2 f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).
 
 Tactic Notation "cofe_subst" ident(x) :=
   repeat match goal with
@@ -87,7 +89,7 @@ Arguments chain_car {_} _ _.
 Arguments chain_cauchy {_} _ _ _ _.
 
 Program Definition chain_map {A B : ofeT} (f : A → B)
-    `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
+    `{!NonExpansive f} (c : chain A) : chain B :=
   {| chain_car n := f (c n) |}.
 Next Obligation. by intros A B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
 
@@ -99,7 +101,7 @@ Class Cofe (A : ofeT) := {
 Arguments compl : simpl never.
 
 Lemma compl_chain_map `{Cofe A, Cofe B} (f : A → B) c
-      `(∀ n : nat, Proper (dist n ==> dist n) f) :
+      `(NonExpansive f) :
   compl (chain_map f c) ≡ f (compl c).
 Proof. apply equiv_dist=>n. by rewrite !conv_compl. Qed.
 
@@ -131,10 +133,10 @@ Section cofe.
   Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
   Proof. intros; eauto using dist_le. Qed.
   Instance ne_proper {B : ofeT} (f : A → B)
-    `{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100.
+    `{!NonExpansive f} : Proper ((≡) ==> (≡)) f | 100.
   Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
   Instance ne_proper_2 {B C : ofeT} (f : A → B → C)
-    `{!∀ n, Proper (dist n ==> dist n ==> dist n) f} :
+    `{!NonExpansive2 f} :
     Proper ((≡) ==> (≡) ==> (≡)) f | 100.
   Proof.
      unfold Proper, respectful; setoid_rewrite equiv_dist.
@@ -175,8 +177,8 @@ Section contractive.
   Lemma contractive_S n x y : x ≡{n}≡ y → f x ≡{S n}≡ f y.
   Proof. intros. by apply (_ : Contractive f). Qed.
 
-  Global Instance contractive_ne n : Proper (dist n ==> dist n) f | 100.
-  Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
+  Global Instance contractive_ne : NonExpansive f | 100.
+  Proof. by intros n x y ?; apply dist_S, contractive_S. Qed.
   Global Instance contractive_proper : Proper ((≡) ==> (≡)) f | 100.
   Proof. apply (ne_proper _). Qed.
 End contractive.
@@ -270,7 +272,7 @@ Section fixpointK.
   Context `{Cofe A, Inhabited A} (f : A → A) (k : nat).
   Context `{f_contractive : !Contractive (Nat.iter k f)}.
   (* TODO: Can we get rid of this assumption, derive it from contractivity? *)
-  Context `{f_ne : !∀ n, Proper (dist n ==> dist n) f}.
+  Context {f_ne : NonExpansive f}.
 
   Let f_proper : Proper ((≡) ==> (≡)) f := ne_proper f.
   Existing Instance f_proper.
@@ -289,7 +291,7 @@ Section fixpointK.
 
   Section fixpointK_ne.
     Context (g : A → A) `{g_contractive : !Contractive (Nat.iter k g)}.
-    Context {g_ne : ∀ n, Proper (dist n ==> dist n) g}.
+    Context {g_ne : NonExpansive g}.
 
     Lemma fixpointK_ne n : (∀ z, f z ≡{n}≡ g z) → fixpointK k f ≡{n}≡ fixpointK k g.
     Proof.
@@ -423,7 +425,7 @@ Instance ofe_fun_inhabited {A} {B : ofeT} `{Inhabited B} :
 (** Non-expansive function space *)
 Record ofe_mor (A B : ofeT) : Type := CofeMor {
   ofe_mor_car :> A → B;
-  ofe_mor_ne n : Proper (dist n ==> dist n) ofe_mor_car
+  ofe_mor_ne : NonExpansive ofe_mor_car
 }.
 Arguments CofeMor {_ _} _ {_}.
 Add Printing Constructor ofe_mor.
@@ -468,9 +470,9 @@ Section ofe_mor.
     by rewrite (conv_compl n (ofe_mor_chain c x)) /=.
   Qed.
 
-  Global Instance ofe_mor_car_ne n :
-    Proper (dist n ==> dist n ==> dist n) (@ofe_mor_car A B).
-  Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
+  Global Instance ofe_mor_car_ne :
+    NonExpansive2 (@ofe_mor_car A B).
+  Proof. intros n f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
   Global Instance ofe_mor_car_proper :
     Proper ((≡) ==> (≡) ==> (≡)) (@ofe_mor_car A B) := ne_proper_2 _.
   Lemma ofe_mor_ext (f g : ofe_mor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
@@ -506,10 +508,10 @@ Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
 
 Definition ofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
   (A -n> B) -n> (A' -n>  B') := CofeMor (ofe_mor_map f g).
-Instance ofe_morC_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n) (@ofe_morC_map A A' B B').
+Instance ofe_morC_map_ne {A A' B B'} :
+  NonExpansive2 (@ofe_morC_map A A' B B').
 Proof.
-  intros f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
+  intros n f f' Hf g g' Hg ?. rewrite /= /ofe_mor_map.
   by repeat apply ccompose_ne.
 Qed.
 
@@ -533,9 +535,9 @@ Section product.
 
   Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
   Global Instance pair_ne :
-    Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
-  Global Instance fst_ne : Proper (dist n ==> dist n) (@fst A B) := _.
-  Global Instance snd_ne : Proper (dist n ==> dist n) (@snd A B) := _.
+    NonExpansive2 (@pair A B) := _.
+  Global Instance fst_ne : NonExpansive (@fst A B) := _.
+  Global Instance snd_ne : NonExpansive (@snd A B) := _.
   Definition prod_ofe_mixin : OfeMixin (A * B).
   Proof.
     split.
@@ -569,17 +571,17 @@ Instance prod_map_ne {A A' B B' : ofeT} n :
 Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed.
 Definition prodC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
   prodC A B -n> prodC A' B' := CofeMor (prod_map f g).
-Instance prodC_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n) (@prodC_map A A' B B').
-Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
+Instance prodC_map_ne {A A' B B'} :
+  NonExpansive2 (@prodC_map A A' B B').
+Proof. intros n f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
 
 (** Functors *)
 Structure cFunctor := CFunctor {
   cFunctor_car : ofeT → ofeT → ofeT;
   cFunctor_map {A1 A2 B1 B2} :
     ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
-  cFunctor_ne {A1 A2 B1 B2} n :
-    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
+  cFunctor_ne {A1 A2 B1 B2} :
+    NonExpansive (@cFunctor_map A1 A2 B1 B2);
   cFunctor_id {A B : ofeT} (x : cFunctor_car A B) :
     cFunctor_map (cid,cid) x ≡ x;
   cFunctor_compose {A1 A2 A3 B1 B2 B3}
@@ -634,15 +636,15 @@ Proof.
     by apply prodC_map_ne; apply cFunctor_contractive.
 Qed.
 
-Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') n :
-  Proper (dist n ==> dist n) (compose f : (A -c> B) → A -c> B').
-Proof. intros g g' Hf x; simpl. by rewrite (Hf x). Qed.
+Instance compose_ne {A} {B B' : ofeT} (f : B -n> B') :
+  NonExpansive (compose f : (A -c> B) → A -c> B').
+Proof. intros n g g' Hf x; simpl. by rewrite (Hf x). Qed.
 
 Definition ofe_funC_map {A B B'} (f : B -n> B') : (A -c> B) -n> (A -c> B') :=
   @CofeMor (_ -c> _) (_ -c> _) (compose f) _.
-Instance ofe_funC_map_ne {A B B'} n :
-  Proper (dist n ==> dist n) (@ofe_funC_map A B B').
-Proof. intros f f' Hf g x. apply Hf. Qed.
+Instance ofe_funC_map_ne {A B B'} :
+  NonExpansive (@ofe_funC_map A B B').
+Proof. intros n f f' Hf g x. apply Hf. Qed.
 
 Program Definition ofe_funCF (T : Type) (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := ofe_funC T (cFunctor_car F A B);
@@ -697,8 +699,8 @@ Section sum.
   Context {A B : ofeT}.
 
   Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
-  Global Instance inl_ne : Proper (dist n ==> dist n) (@inl A B) := _.
-  Global Instance inr_ne : Proper (dist n ==> dist n) (@inr A B) := _.
+  Global Instance inl_ne : NonExpansive (@inl A B) := _.
+  Global Instance inr_ne : NonExpansive (@inr A B) := _.
   Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _.
   Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _.
 
@@ -753,9 +755,9 @@ Proof.
 Qed.
 Definition sumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
   sumC A B -n> sumC A' B' := CofeMor (sum_map f g).
-Instance sumC_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n) (@sumC_map A A' B B').
-Proof. intros f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.
+Instance sumC_map_ne {A A' B B'} :
+  NonExpansive2 (@sumC_map A A' B B').
+Proof. intros n f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.
 
 Program Definition sumCF (F1 F2 : cFunctor) : cFunctor := {|
   cFunctor_car A B := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
@@ -852,7 +854,7 @@ Section option.
   Global Instance option_discrete : Discrete A → Discrete optionC.
   Proof. destruct 2; constructor; by apply (timeless _). Qed.
 
-  Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
+  Global Instance Some_ne : NonExpansive (@Some A).
   Proof. by constructor. Qed.
   Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
   Proof. destruct 1; split; eauto. Qed.
@@ -889,8 +891,8 @@ Instance option_fmap_ne {A B : ofeT} n:
 Proof. intros f f' Hf ?? []; constructor; auto. Qed.
 Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
   CofeMor (fmap f : optionC A → optionC B).
-Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
-Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
+Instance optionC_map_ne A B : NonExpansive (@optionC_map A B).
+Proof. by intros n f f' Hf []; constructor; apply Hf. Qed.
 
 Program Definition optionCF (F : cFunctor) : cFunctor := {|
   cFunctor_car A B := optionC (cFunctor_car F A B);
@@ -959,7 +961,7 @@ Section later.
   (* f is contractive iff it can factor into `Next` and a non-expansive function. *)
   Lemma contractive_alt {B : ofeT} (f : A → B) :
     Contractive f ↔ ∃ g : later A → B,
-      (∀ n, Proper (dist n ==> dist n) g) ∧ (∀ x, f x ≡ g (Next x)).
+      (NonExpansive g) ∧ (∀ x, f x ≡ g (Next x)).
   Proof.
     split.
     - intros Hf. exists (f ∘ later_car); split=> // n x y ?. by f_equiv.
@@ -1042,7 +1044,7 @@ Section sigma.
   Lemma exist_ne n a1 a2 (H1 : P a1) (H2 : P a2) :
     a1 ≡{n}≡ a2 → a1 ↾ H1 ≡{n}≡ a2 ↾ H2.
   Proof. done. Qed.
-  Global Instance proj1_sig_ne : Proper (dist n ==> dist n) (@proj1_sig _ P).
+  Global Instance proj1_sig_ne : NonExpansive (@proj1_sig _ P).
   Proof. by intros n [a Ha] [b Hb] ?. Qed.
   Definition sig_ofe_mixin : OfeMixin (sig P).
   Proof.
diff --git a/theories/algebra/vector.v b/theories/algebra/vector.v
index 1ee6ef12d4adb8989b9fff01017e7cad58f8c654..032779915bc471cb781c798d89895720f13f4500 100644
--- a/theories/algebra/vector.v
+++ b/theories/algebra/vector.v
@@ -57,8 +57,8 @@ Section proper.
     intros v v' ? x x' ->. apply equiv_dist=> n. f_equiv. by apply equiv_dist.
   Qed.
 
-  Global Instance vec_to_list_ne n m :
-    Proper (dist n ==> dist n) (@vec_to_list A m).
+  Global Instance vec_to_list_ne m :
+    NonExpansive (@vec_to_list A m).
   Proof. by intros v v'. Qed.
   Global Instance vec_to_list_proper m :
     Proper (equiv ==> equiv) (@vec_to_list A m).
@@ -99,9 +99,9 @@ Proof.
 Qed.
 Definition vecC_map {A B : ofeT} m (f : A -n> B) : vecC A m -n> vecC B m :=
   CofeMor (vec_map m f).
-Instance vecC_map_ne {A A'} m n :
-  Proper (dist n ==> dist n) (@vecC_map A A' m).
-Proof. intros f g ? v. by apply vec_map_ext_ne. Qed.
+Instance vecC_map_ne {A A'} m :
+  NonExpansive (@vecC_map A A' m).
+Proof. intros n f g ? v. by apply vec_map_ext_ne. Qed.
 
 Program Definition vecCF (F : cFunctor) m : cFunctor := {|
   cFunctor_car A B := vecC (cFunctor_car F A B) m;
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index c812280a89ef8419a483d55caa9ebdcc45d729e4..bb4f7fa2a29ae4f3ab469bef17cefc077a8b68d4 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -321,7 +321,7 @@ Proof.
   apply or_elim. by rewrite -(exist_intro true). by rewrite -(exist_intro false).
 Qed.
 
-Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
+Global Instance iff_ne : NonExpansive2 (@uPred_iff M).
 Proof. unfold uPred_iff; solve_proper. Qed.
 Global Instance iff_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_iff M) := ne_proper_2 _.
@@ -579,7 +579,7 @@ Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
 
 
 (* Iterated later modality *)
-Global Instance laterN_ne n m : Proper (dist n ==> dist n) (@uPred_laterN M m).
+Global Instance laterN_ne m : NonExpansive (@uPred_laterN M m).
 Proof. induction m; simpl. by intros ???. solve_proper. Qed.
 Global Instance laterN_proper m :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_laterN M m) := ne_proper _.
@@ -631,7 +631,7 @@ Lemma laterN_iff n P Q : ▷^n (P ↔ Q) ⊢ ▷^n P ↔ ▷^n Q.
 Proof. by rewrite /uPred_iff laterN_and !laterN_impl. Qed.
 
 (* Conditional always *)
-Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
+Global Instance always_if_ne p : NonExpansive (@uPred_always_if M p).
 Proof. solve_proper. Qed.
 Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
 Proof. solve_proper. Qed.
@@ -658,7 +658,7 @@ Proof. destruct p; simpl; auto using always_later. Qed.
 
 
 (* True now *)
-Global Instance except_0_ne n : Proper (dist n ==> dist n) (@uPred_except_0 M).
+Global Instance except_0_ne : NonExpansive (@uPred_except_0 M).
 Proof. solve_proper. Qed.
 Global Instance except_0_proper : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_except_0 M).
 Proof. solve_proper. Qed.
diff --git a/theories/base_logic/double_negation.v b/theories/base_logic/double_negation.v
index fb692ba9a260e11e9e3fc825d420d9fb2d5b07a9..72977057e15071c01f38531eab068b873ffc400e 100644
--- a/theories/base_logic/double_negation.v
+++ b/theories/base_logic/double_negation.v
@@ -217,8 +217,8 @@ Qed.
 Instance nnupd_k_mono' k: Proper ((⊢) ==> (⊢)) (@uPred_nnupd_k M k).
 Proof. by intros P P' HP; apply nnupd_k_mono. Qed.
 
-Instance nnupd_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnupd_k M k).
-Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
+Instance nnupd_k_ne k : NonExpansive (@uPred_nnupd_k M k).
+Proof. intros n. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
 Lemma nnupd_k_proper k P Q: (P ⊣⊢ Q) → (|=n=>_k P) ⊣⊢ (|=n=>_k Q).
 Proof. intros HP; apply (anti_symm (⊢)); eapply nnupd_k_mono; by rewrite HP. Qed.
 Instance nnupd_k_proper' k: Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_nnupd_k M k).
diff --git a/theories/base_logic/lib/auth.v b/theories/base_logic/lib/auth.v
index 1ad2380301cbb2264bdf97e8e0cae2e85ae08784..d5638eeb0de494a271d9d4766bced126e40f33fe 100644
--- a/theories/base_logic/lib/auth.v
+++ b/theories/base_logic/lib/auth.v
@@ -26,7 +26,7 @@ Section definitions.
   Definition auth_ctx (N : namespace) (f : T → A) (φ : T → iProp Σ) : iProp Σ :=
     inv N (auth_inv f φ).
 
-  Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
+  Global Instance auth_own_ne : NonExpansive auth_own.
   Proof. solve_proper. Qed.
   Global Instance auth_own_proper : Proper ((≡) ==> (⊣⊢)) auth_own.
   Proof. solve_proper. Qed.
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 7b1615c3a119bf6274e9184d359f4086ec09916b..0722ee82331455c7c85cf8da7d4ecec0cf1caa6c 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -51,15 +51,15 @@ Section box.
 Context `{invG Σ, boxG Σ} (N : namespace).
 Implicit Types P Q : iProp Σ.
 
-Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
+Global Instance box_own_prop_ne γ : NonExpansive (box_own_prop γ).
 Proof. solve_proper. Qed.
 Global Instance box_own_prop_contractive γ : Contractive (box_own_prop γ).
 Proof. solve_contractive. Qed.
 
-Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
+Global Instance box_inv_ne γ : NonExpansive (slice_inv γ).
 Proof. solve_proper. Qed.
 
-Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ).
+Global Instance slice_ne γ : NonExpansive (slice N γ).
 Proof. solve_proper. Qed.
 Global Instance slice_contractive γ : Contractive (slice N γ).
 Proof. solve_contractive. Qed.
@@ -69,7 +69,7 @@ Proof. apply _. Qed.
 
 Global Instance box_contractive f : Contractive (box N f).
 Proof. solve_contractive. Qed.
-Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f).
+Global Instance box_ne f : NonExpansive (box N f).
 Proof. apply (contractive_ne _). Qed.
 
 Lemma box_own_auth_agree γ b1 b2 :
diff --git a/theories/base_logic/lib/cancelable_invariants.v b/theories/base_logic/lib/cancelable_invariants.v
index c06067a316eff18ce774362c4f62191b46fba593..451fb5b0e464ed5063b803fdffe93b032335cf3d 100644
--- a/theories/base_logic/lib/cancelable_invariants.v
+++ b/theories/base_logic/lib/cancelable_invariants.v
@@ -24,7 +24,7 @@ Section proofs.
   Global Instance cinv_own_timeless γ p : TimelessP (cinv_own γ p).
   Proof. rewrite /cinv_own; apply _. Qed.
 
-  Global Instance cinv_ne N γ n : Proper (dist n ==> dist n) (cinv N γ).
+  Global Instance cinv_ne N γ : NonExpansive (cinv N γ).
   Proof. solve_proper. Qed.
   Global Instance cinv_proper N γ : Proper ((≡) ==> (≡)) (cinv N γ).
   Proof. apply (ne_proper _). Qed.
diff --git a/theories/base_logic/lib/fancy_updates.v b/theories/base_logic/lib/fancy_updates.v
index d772d0faad48eca058eb9a0adf2693d6921360df..37308769dcd0ba3bd5cebf294f3015501d421016 100644
--- a/theories/base_logic/lib/fancy_updates.v
+++ b/theories/base_logic/lib/fancy_updates.v
@@ -39,7 +39,7 @@ Section fupd.
 Context `{invG Σ}.
 Implicit Types P Q : iProp Σ.
 
-Global Instance fupd_ne E1 E2 n : Proper (dist n ==> dist n) (@fupd Σ _ E1 E2).
+Global Instance fupd_ne E1 E2 : NonExpansive (@fupd Σ _ E1 E2).
 Proof. rewrite fupd_eq. solve_proper. Qed.
 Global Instance fupd_proper E1 E2 : Proper ((≡) ==> (≡)) (@fupd Σ _ E1 E2).
 Proof. apply ne_proper, _. Qed.
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index 6f760c91e99054dcd13a67d8977c69959a4526b2..39fb911ddc3e9b91b85a84a5f7c6fa2c3fcfa311 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/theories/base_logic/lib/na_invariants.v
@@ -35,7 +35,7 @@ Section proofs.
   Global Instance na_own_timeless p E : TimelessP (na_own p E).
   Proof. rewrite /na_own; apply _. Qed.
 
-  Global Instance na_inv_ne p N n : Proper (dist n ==> dist n) (na_inv p N).
+  Global Instance na_inv_ne p N : NonExpansive (na_inv p N).
   Proof. rewrite /na_inv. solve_proper. Qed.
   Global Instance na_inv_proper p N : Proper ((≡) ==> (≡)) (na_inv p N).
   Proof. apply (ne_proper _). Qed.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index dfcca18ca7ece752d8f93e1439755e322fd8638d..24c20fae6444db93559828ad2ba7b0d5f997d6ce 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -66,9 +66,9 @@ Context `{inG Σ A}.
 Implicit Types a : A.
 
 (** ** Properties of [iRes_singleton] *)
-Global Instance iRes_singleton_ne γ n :
-  Proper (dist n ==> dist n) (@iRes_singleton Σ A _ γ).
-Proof. by intros a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
+Global Instance iRes_singleton_ne γ :
+  NonExpansive (@iRes_singleton Σ A _ γ).
+Proof. by intros n a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
 Lemma iRes_singleton_op γ a1 a2 :
   iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
 Proof.
@@ -76,7 +76,7 @@ Proof.
 Qed.
 
 (** ** Properties of [own] *)
-Global Instance own_ne γ n : Proper (dist n ==> dist n) (@own Σ A _ γ).
+Global Instance own_ne γ : NonExpansive (@own Σ A _ γ).
 Proof. rewrite !own_eq. solve_proper. Qed.
 Global Instance own_proper γ :
   Proper ((≡) ==> (⊣⊢)) (@own Σ A _ γ) := ne_proper _.
diff --git a/theories/base_logic/lib/viewshifts.v b/theories/base_logic/lib/viewshifts.v
index 906965920c1c12652cfea4b8ced04247db6564a6..b786ec65adac7ee76d8f14952878734f452b2c9f 100644
--- a/theories/base_logic/lib/viewshifts.v
+++ b/theories/base_logic/lib/viewshifts.v
@@ -26,7 +26,7 @@ Context `{invG Σ}.
 Implicit Types P Q R : iProp Σ.
 Implicit Types N : namespace.
 
-Global Instance vs_ne E1 E2 n: Proper (dist n ==> dist n ==> dist n) (vs E1 E2).
+Global Instance vs_ne E1 E2 : NonExpansive2 (vs E1 E2).
 Proof. solve_proper. Qed.
 
 Global Instance vs_proper E1 E2 : Proper ((≡) ==> (≡) ==> (≡)) (vs E1 E2).
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index d145a96b0233923d31f46109a0bcba18cca94c54..b471bfdaf41aed9c03752a96ecb401e42ee185cc 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -213,49 +213,49 @@ Hint Immediate uPred_in_entails.
 (** Non-expansiveness and setoid morphisms *)
 Global Instance pure_proper : Proper (iff ==> (⊣⊢)) (@uPred_pure M).
 Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|n] ?; try apply Hφ. Qed.
-Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
+Global Instance and_ne : NonExpansive2 (@uPred_and M).
 Proof.
-  intros P P' HP Q Q' HQ; unseal; split=> x n' ??.
+  intros n P P' HP Q Q' HQ; unseal; split=> x n' ??.
   split; (intros [??]; split; [by apply HP|by apply HQ]).
 Qed.
 Global Instance and_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_and M) := ne_proper_2 _.
-Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
+Global Instance or_ne : NonExpansive2 (@uPred_or M).
 Proof.
-  intros P P' HP Q Q' HQ; split=> x n' ??.
+  intros n P P' HP Q Q' HQ; split=> x n' ??.
   unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
 Qed.
 Global Instance or_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_or M) := ne_proper_2 _.
-Global Instance impl_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
+Global Instance impl_ne :
+  NonExpansive2 (@uPred_impl M).
 Proof.
-  intros P P' HP Q Q' HQ; split=> x n' ??.
+  intros n P P' HP Q Q' HQ; split=> x n' ??.
   unseal; split; intros HPQ x' n'' ????; apply HQ, HPQ, HP; auto.
 Qed.
 Global Instance impl_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_impl M) := ne_proper_2 _.
-Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
+Global Instance sep_ne : NonExpansive2 (@uPred_sep M).
 Proof.
-  intros P P' HP Q Q' HQ; split=> n' x ??.
+  intros n P P' HP Q Q' HQ; split=> n' x ??.
   unseal; split; intros (x1&x2&?&?&?); cofe_subst x;
     exists x1, x2; split_and!; try (apply HP || apply HQ);
     eauto using cmra_validN_op_l, cmra_validN_op_r.
 Qed.
 Global Instance sep_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_sep M) := ne_proper_2 _.
-Global Instance wand_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
+Global Instance wand_ne :
+  NonExpansive2 (@uPred_wand M).
 Proof.
-  intros P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
+  intros n P P' HP Q Q' HQ; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
     apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
 Qed.
 Global Instance wand_proper :
   Proper ((⊣⊢) ==> (⊣⊢) ==> (⊣⊢)) (@uPred_wand M) := ne_proper_2 _.
-Global Instance internal_eq_ne (A : ofeT) n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_internal_eq M A).
+Global Instance internal_eq_ne (A : ofeT) :
+  NonExpansive2 (@uPred_internal_eq M A).
 Proof.
-  intros x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
+  intros n x x' Hx y y' Hy; split=> n' z; unseal; split; intros; simpl in *.
   - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
   - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
 Qed.
@@ -290,30 +290,30 @@ Proof.
 Qed.
 Global Instance later_proper' :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_later M) := ne_proper _.
-Global Instance always_ne n : Proper (dist n ==> dist n) (@uPred_always M).
+Global Instance always_ne : NonExpansive (@uPred_always M).
 Proof.
-  intros P1 P2 HP.
+  intros n P1 P2 HP.
   unseal; split=> n' x; split; apply HP; eauto using @cmra_core_validN.
 Qed.
 Global Instance always_proper :
   Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always M) := ne_proper _.
-Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
+Global Instance ownM_ne : NonExpansive (@uPred_ownM M).
 Proof.
-  intros a b Ha.
+  intros n a b Ha.
   unseal; split=> n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia.
 Qed.
 Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
-Global Instance cmra_valid_ne {A : cmraT} n :
-Proper (dist n ==> dist n) (@uPred_cmra_valid M A).
+Global Instance cmra_valid_ne {A : cmraT} :
+  NonExpansive (@uPred_cmra_valid M A).
 Proof.
-  intros a b Ha; unseal; split=> n' x ? /=.
+  intros n a b Ha; unseal; split=> n' x ? /=.
   by rewrite (dist_le _ _ _ _ Ha); last lia.
 Qed.
 Global Instance cmra_valid_proper {A : cmraT} :
   Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
-Global Instance bupd_ne n : Proper (dist n ==> dist n) (@uPred_bupd M).
+Global Instance bupd_ne : NonExpansive (@uPred_bupd M).
 Proof.
-  intros P Q HPQ.
+  intros n P Q HPQ.
   unseal; split=> n' x; split; intros HP k yf ??;
     destruct (HP k yf) as (x'&?&?); auto;
     exists x'; split; auto; apply HPQ; eauto using cmra_validN_op_l.
@@ -370,7 +370,7 @@ Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
 Lemma internal_eq_refl {A : ofeT} (a : A) : uPred_valid (M:=M) (a ≡ a).
 Proof. unseal; by split=> n x ??; simpl. Qed.
 Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) P
-  {HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
+  {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
   unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
   - by symmetry; apply Hab with x.
diff --git a/theories/heap_lang/lib/barrier/proof.v b/theories/heap_lang/lib/barrier/proof.v
index c94a47a4339e4b682fc2e0945c1ad786293be5d4..cfc90fab86ae1d88328f54d2d92e90ec7961ad3f 100644
--- a/theories/heap_lang/lib/barrier/proof.v
+++ b/theories/heap_lang/lib/barrier/proof.v
@@ -55,17 +55,17 @@ Proof. apply _. Qed.
 (** Setoids *)
 Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
 Proof. solve_proper. Qed.
-Global Instance state_to_prop_ne n s :
-  Proper (dist n ==> dist n) (state_to_prop s).
+Global Instance state_to_prop_ne s :
+  NonExpansive (state_to_prop s).
 Proof. solve_proper. Qed.
 Global Instance barrier_inv_ne n l :
   Proper (dist n ==> eq ==> dist n) (barrier_inv l).
 Proof. solve_proper. Qed.
-Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
+Global Instance barrier_ctx_ne γ l : NonExpansive (barrier_ctx γ l).
 Proof. solve_proper. Qed. 
-Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
+Global Instance send_ne l : NonExpansive (send l).
 Proof. solve_proper. Qed.
-Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
+Global Instance recv_ne l : NonExpansive (recv l).
 Proof. solve_proper. Qed.
 
 (** Helper lemmas *)
diff --git a/theories/heap_lang/lib/lock.v b/theories/heap_lang/lib/lock.v
index dcae7f0acb3bc8def110d8d46fd062001d85a838..f16c450e468d45fc1a527d940249e6863ad888ca 100644
--- a/theories/heap_lang/lib/lock.v
+++ b/theories/heap_lang/lib/lock.v
@@ -13,7 +13,7 @@ Structure lock Σ `{!heapG Σ} := Lock {
   is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
   locked (γ: name) : iProp Σ;
   (* -- general properties -- *)
-  is_lock_ne N γ lk n: Proper (dist n ==> dist n) (is_lock N γ lk);
+  is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
   is_lock_persistent N γ lk R : PersistentP (is_lock N γ lk R);
   locked_timeless γ : TimelessP (locked γ);
   locked_exclusive γ : locked γ -∗ locked γ -∗ False;
diff --git a/theories/heap_lang/lib/spin_lock.v b/theories/heap_lang/lib/spin_lock.v
index 4d70eb77b30a0b99d85af9879490d0523a21a397..65375c186666ecc2b3813a828b6a634f2c7cfac0 100644
--- a/theories/heap_lang/lib/spin_lock.v
+++ b/theories/heap_lang/lib/spin_lock.v
@@ -34,9 +34,9 @@ Section proof.
   Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
   Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
 
-  Global Instance lock_inv_ne n γ l : Proper (dist n ==> dist n) (lock_inv γ l).
+  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_ne n l : Proper (dist n ==> dist n) (is_lock γ l).
+  Global Instance is_lock_ne l : NonExpansive (is_lock γ l).
   Proof. solve_proper. Qed.
 
   (** The main proofs. *)
diff --git a/theories/heap_lang/lib/ticket_lock.v b/theories/heap_lang/lib/ticket_lock.v
index 2900b73c4488b9e8489ad0eea01ae453773dd687..3ec347a77a46337d23ed684b025f39da205fe60e 100644
--- a/theories/heap_lang/lib/ticket_lock.v
+++ b/theories/heap_lang/lib/ticket_lock.v
@@ -56,10 +56,10 @@ Section proof.
 
   Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, ∅)))%I.
 
-  Global Instance lock_inv_ne n γ lo ln :
-    Proper (dist n ==> dist n) (lock_inv γ lo ln).
+  Global Instance lock_inv_ne γ lo ln :
+    NonExpansive (lock_inv γ lo ln).
   Proof. solve_proper. Qed.
-  Global Instance is_lock_ne γ n lk : Proper (dist n ==> dist n) (is_lock γ lk).
+  Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
   Proof. solve_proper. Qed.
   Global Instance is_lock_persistent γ lk R : PersistentP (is_lock γ lk R).
   Proof. apply _. Qed.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 0cb4f409cc827151b3bd8d309a04bc1efb50bafc..bb4489e5eca99d6bb84ff329c5078b7e08cd34c6 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -30,7 +30,7 @@ Implicit Types v : val Λ.
 Import uPred.
 
 Global Instance ht_ne E n :
-  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (ht E).
+  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht E).
 Proof. solve_proper. Qed.
 Global Instance ht_proper E :
   Proper ((≡) ==> eq ==> pointwise_relation _ (≡) ==> (≡)) (ht E).
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index b78dad5245e046f47c6eaebb83a4f4b7d02316b6..724615853105ceaa7d586461ba0af5e909ac3494 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -655,7 +655,7 @@ Lemma tac_rewrite Δ i p Pxy (lr : bool) Q :
   ∀ {A : ofeT} (x y : A) (Φ : A → uPred M),
     (Pxy ⊢ x ≡ y) →
     (Q ⊣⊢ Φ (if lr then y else x)) →
-    (∀ n, Proper (dist n ==> dist n) Φ) →
+    (NonExpansive Φ) →
     (Δ ⊢ Φ (if lr then x else y)) → Δ ⊢ Q.
 Proof.
   intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite; auto.
@@ -669,7 +669,7 @@ Lemma tac_rewrite_in Δ i p Pxy j q P (lr : bool) Q :
   ∀ {A : ofeT} Δ' x y (Φ : A → uPred M),
     (Pxy ⊢ x ≡ y) →
     (P ⊣⊢ Φ (if lr then y else x)) →
-    (∀ n, Proper (dist n ==> dist n) Φ) →
+    (NonExpansive Φ) →
     envs_simple_replace j q (Esnoc Enil j (Φ (if lr then x else y))) Δ = Some Δ' →
     (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.