diff --git a/coq-iris.opam b/coq-iris.opam
index a6da172a1ed47659080b8c098095ad4281722e82..db729d1888035fc8d7a06c5af49f757f8302f6ae 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2022-01-13.0.607ee2b1") | (= "dev") }
+  "coq-stdpp" { (= "dev.2022-01-14.1.ac02dbbd") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 0d1b2a7fca60764a4a8a635100141901fe1e2a2d..f5e61a3c1faee9b8c9eaacbb9111d313fc80abfd 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -52,8 +52,11 @@ Lemma cmra_update_exclusive `{!Exclusive x} y:
 Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
 
 (** Updates form a preorder. *)
+(** We set this rewrite relation's priority below the stdlib's 
+  ([impl], [iff], [eq], ...) and [≡] but above [⊑].
+  [eq] (at 100) < [≡] (at 150) < [cmra_update] (at 170) < [⊑] (at 200) *)
 Global Instance cmra_update_rewrite_relation :
-  RewriteRelation (@cmra_update A) := {}.
+  RewriteRelation (@cmra_update A) | 170 := {}.
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof.
   split.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 3317c511c6bfc70a2dbc4ef288a4c7820da02266..90ec924a2ebd354f79c8f7ef9635690b0d6634f1 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -224,7 +224,11 @@ Global Arguments bi_persistently {PROP} _ : simpl never, rename.
 Global Arguments bi_later {PROP} _ : simpl never, rename.
 
 Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
-Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
+(** We set this rewrite relation's priority below the stdlib's 
+  ([impl], [iff], [eq], ...) and [≡] but above [⊑].
+  [eq] (at 100) < [≡] (at 150) < [bi_entails _] (at 170) < [⊑] (at 200)
+*)
+Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) | 170 := {}.
 Global Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
 Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.