diff --git a/coq-iris.opam b/coq-iris.opam
index 87c09486f438be63161ccd7c7e9b354c206bb2d8..f16147e1d894a562108e09b474885324859f2d70 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -14,7 +14,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
 
 depends: [
   "coq" { (>= "8.11" & < "8.14~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-01-28.1.889d99ae") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-02-01.1.bcebd707") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index 5dd69ba7813cbb1155d8b34acb09c6108807cf1a..45e3cbb84e16a5077417ef7af88c711833d9be36 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -409,7 +409,7 @@ Qed.
 
 Lemma dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) = dom _ m1 ∪ dom _ m2.
 Proof.
-  apply elem_of_equiv_L=> i; rewrite elem_of_union !elem_of_dom.
+  apply set_eq=> i; rewrite elem_of_union !elem_of_dom.
   unfold is_Some; setoid_rewrite lookup_op.
   destruct (m1 !! i), (m2 !! i); naive_solver.
 Qed.
diff --git a/iris/algebra/sts.v b/iris/algebra/sts.v
index bac537bb9b322b64dc4e21620a818c0366c93ce3..06c86aaf2aa23f327f8c8e236c616e6713b773c2 100644
--- a/iris/algebra/sts.v
+++ b/iris/algebra/sts.v
@@ -68,7 +68,7 @@ Proof.
     eauto with sts; set_solver.
 Qed.
 Global Instance frame_step_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
-Proof. move=> ?? /set_equiv_spec [??]; split; by apply frame_step_mono. Qed.
+Proof. move=> ?? /set_equiv_subseteq [??]; split; by apply frame_step_mono. Qed.
 Local Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
 Proof. destruct 3; constructor; intros; setoid_subst; eauto. Qed.
 Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
@@ -81,7 +81,7 @@ Proof.
 Qed.
 Global Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
 Proof.
-  by move=> ??? ?? /set_equiv_spec [??]; split; apply up_preserving.
+  by move=> ??? ?? /set_equiv_subseteq [??]; split; apply up_preserving.
 Qed.
 Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
 Proof.
@@ -90,7 +90,7 @@ Proof.
 Qed.
 Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
 Proof.
-  move=> S1 S2 /set_equiv_spec [??] T1 T2 /set_equiv_spec [??];
+  move=> S1 S2 /set_equiv_subseteq [??] T1 T2 /set_equiv_subseteq [??];
     split; by apply up_set_preserving.
 Qed.
 
@@ -155,7 +155,7 @@ Lemma closed_up_empty s : closed (up s ∅) ∅.
 Proof. eauto using closed_up with sts. Qed.
 Lemma up_closed S T : closed S T → up_set S T ≡ S.
 Proof.
-  intros ?; apply set_equiv_spec; split; auto using subseteq_up_set.
+  intros ?; apply set_equiv_subseteq; split; auto using subseteq_up_set.
   intros s; unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
   induction Hstep; eauto using closed_step.
 Qed.
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index dd131871677ad710d199e1830a397c6cdeb9bbf1..67c4e5393910eaefa927801c2e691e27bca131a8 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1333,7 +1333,7 @@ Section map2.
     ⌜ dom (gset K) m1 = dom (gset K) m2 ⌝.
   Proof.
     rewrite big_sepM2_lookup_iff. apply pure_mono=>Hm.
-    apply elem_of_equiv_L=> k. by rewrite !elem_of_dom.
+    apply set_eq=> k. by rewrite !elem_of_dom.
   Qed.
 
   Lemma big_sepM2_flip Φ m1 m2 :