diff --git a/coq-iris.opam b/coq-iris.opam
index faed3ff40a03978dfb8a873601ca02148589831c..07f5e11b1a641e37e7d7266542146243148624bf 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -15,7 +15,7 @@ iris.prelude, iris.algebra, iris.si_logic, iris.bi, iris.proofmode, iris.base_lo
 
 depends: [
   "coq" { (>= "8.12" & < "8.14~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-06-16.0.fc5f75e5") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-06-17.3.3bddee70") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 5dde79ec0062a1db155c08bc5836e40071a0b7a5..07f46ded4e3119ff2d9166cd72695e2ee8af4ef3 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -341,13 +341,13 @@ Proof. rewrite !cmra_valid_validN; eauto using cmra_validN_op_r. Qed.
 
 (** ** Core *)
 Lemma cmra_pcore_l' x cx : pcore x ≡ Some cx → cx ⋅ x ≡ x.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_l. Qed.
+Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_l. Qed.
 Lemma cmra_pcore_r x cx : pcore x = Some cx → x ⋅ cx ≡ x.
 Proof. intros. rewrite comm. by apply cmra_pcore_l. Qed.
 Lemma cmra_pcore_r' x cx : pcore x ≡ Some cx → x ⋅ cx ≡ x.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. by apply cmra_pcore_r. Qed.
+Proof. intros (cx'&?&<-)%Some_equiv_eq. by apply cmra_pcore_r. Qed.
 Lemma cmra_pcore_idemp' x cx : pcore x ≡ Some cx → pcore cx ≡ Some cx.
-Proof. intros (cx'&?&->)%equiv_Some_inv_r'. eauto using cmra_pcore_idemp. Qed.
+Proof. intros (cx'&?&<-)%Some_equiv_eq. eauto using cmra_pcore_idemp. Qed.
 Lemma cmra_pcore_dup x cx : pcore x = Some cx → cx ≡ cx ⋅ cx.
 Proof. intros; symmetry; eauto using cmra_pcore_r', cmra_pcore_idemp. Qed.
 Lemma cmra_pcore_dup' x cx : pcore x ≡ Some cx → cx ≡ cx ⋅ cx.
@@ -412,9 +412,9 @@ Proof. rewrite (comm op); apply cmra_included_l. Qed.
 Lemma cmra_pcore_mono' x y cx :
   x ≼ y → pcore x ≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy.
 Proof.
-  intros ? (cx'&?&Hcx)%equiv_Some_inv_r'.
+  intros ? (cx'&?&Hcx)%Some_equiv_eq.
   destruct (cmra_pcore_mono x y cx') as (cy&->&?); auto.
-  exists cy; by rewrite Hcx.
+  exists cy; by rewrite -Hcx.
 Qed.
 Lemma cmra_pcore_monoN' n x y cx :
   x ≼{n} y → pcore x ≡{n}≡ Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼{n} cy.
@@ -1126,7 +1126,7 @@ Section prod.
   Lemma prod_pcore_Some' (x cx : A * B) :
     pcore x ≡ Some cx ↔ pcore (x.1) ≡ Some (cx.1) ∧ pcore (x.2) ≡ Some (cx.2).
   Proof.
-    split; [by intros (cx'&[-> ->]%prod_pcore_Some&->)%equiv_Some_inv_r'|].
+    split; [by intros (cx'&[-> ->]%prod_pcore_Some&<-)%Some_equiv_eq|].
     rewrite {3}/pcore /prod_pcore_instance. (* TODO: use setoid rewrite *)
     intros [Hx1 Hx2]; inversion_clear Hx1; simpl; inversion_clear Hx2.
     by constructor.
diff --git a/iris/algebra/cmra_big_op.v b/iris/algebra/cmra_big_op.v
index 71236bbaaa72332c3592272c483e828eef249943..282094e776c595055e6b6f1c144de9211f32cd93 100644
--- a/iris/algebra/cmra_big_op.v
+++ b/iris/algebra/cmra_big_op.v
@@ -14,7 +14,7 @@ Lemma big_opM_None {M : cmra} `{Countable K} {A} (f : K → A → option M) m :
   ([^op map] k↦x ∈ m, f k x) = None ↔ ∀ k x, m !! k = Some x → f k x = None.
 Proof.
   induction m as [|i x m ? IH] using map_ind=> /=; first by rewrite big_opM_eq.
-  rewrite -equiv_None big_opM_insert // equiv_None op_None IH. split.
+  rewrite -None_equiv_eq big_opM_insert // None_equiv_eq op_None IH. split.
   { intros [??] k y. rewrite lookup_insert_Some; naive_solver. }
   intros Hm; split.
   - apply (Hm i). by simplify_map_eq.
@@ -24,13 +24,13 @@ Lemma big_opS_None {M : cmra} `{Countable A} (f : A → option M) X :
   ([^op set] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
   induction X as [|x X ? IH] using set_ind_L; [by rewrite big_opS_eq |].
-  rewrite -equiv_None big_opS_insert // equiv_None op_None IH. set_solver.
+  rewrite -None_equiv_eq big_opS_insert // None_equiv_eq op_None IH. set_solver.
 Qed.
 Lemma big_opMS_None {M : cmra} `{Countable A} (f : A → option M) X :
   ([^op mset] x ∈ X, f x) = None ↔ ∀ x, x ∈ X → f x = None.
 Proof.
   induction X as [|x X IH] using gmultiset_ind.
   { rewrite big_opMS_empty. multiset_solver. }
-  rewrite -equiv_None big_opMS_disj_union big_opMS_singleton equiv_None op_None IH.
+  rewrite -None_equiv_eq big_opMS_disj_union big_opMS_singleton None_equiv_eq op_None IH.
   multiset_solver.
 Qed.
diff --git a/iris/algebra/gmap.v b/iris/algebra/gmap.v
index a61482362eb7dc35455ed4883b7ec8fd4703e30c..55c589952bca7a858691b65aa8090ae5f7e9d351 100644
--- a/iris/algebra/gmap.v
+++ b/iris/algebra/gmap.v
@@ -299,7 +299,7 @@ Proof. apply omap_singleton_Some. Qed.
 Lemma singleton_core' (i : K) (x : A) cx :
   pcore x ≡ Some cx → core {[ i := x ]} ≡@{gmap K A} {[ i := cx ]}.
 Proof.
-  intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (singleton_core _ _ cx').
+  intros (cx'&?&<-)%Some_equiv_eq. by rewrite (singleton_core _ _ cx').
 Qed.
 Lemma singleton_core_total `{!CmraTotal A} (i : K) (x : A) :
   core {[ i := x ]} =@{gmap K A} {[ i := core x ]}.