diff --git a/theories/base_logic/bi.v b/theories/base_logic/bi.v
index 3b7ce4c72629c47f88247edf7f9709de31bf1efc..1b7fdb09dd1713dc4c55bbb7390d58783e760de7 100644
--- a/theories/base_logic/bi.v
+++ b/theories/base_logic/bi.v
@@ -167,8 +167,9 @@ Implicit Types A : Type.
 Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
 Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
 
-Global Existing Instance uPred_primitive.ownM_ne.
-Global Existing Instance uPred_primitive.cmra_valid_ne.
+Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
+Global Instance cmra_valid_ne {A : cmraT} : NonExpansive (@uPred_cmra_valid M A)
+  := uPred_primitive.cmra_valid_ne.
 
 (** Re-exporting primitive Own and valid lemmas *)
 Lemma ownM_op (a1 a2 : M) :