diff --git a/coq-iris.opam b/coq-iris.opam
index c6b6c48a091ac2c845b5651746a4586fbbff9c12..9f5025d9cb45f0a40861b16016d95df2539823e2 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.12" & < "8.16~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2021-12-08.0.130789ac") | (= "dev") }
+  "coq-stdpp" { (= "dev.2021-12-09.0.e6194e28") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris_heap_lang/proph_erasure.v b/iris_heap_lang/proph_erasure.v
index 8d96b7b0050f30faf7a52fcabced727c2360809f..dec08622053fc52ff5d70c0d06acc16c7ede115a 100644
--- a/iris_heap_lang/proph_erasure.v
+++ b/iris_heap_lang/proph_erasure.v
@@ -185,10 +185,10 @@ Proof.
     split; [intros ?|intros (?&?&?)];
       repeat (case_match; simplify_eq/=); eauto.
   - eexists _; split; eauto; simpl.
-    erewrite bool_decide_iff; first by eauto.
+    erewrite bool_decide_ext; first by eauto.
     rewrite erase_val_inj_iff; done.
   - by assert (vals_compare_safe v1 v2) by by apply vals_compare_safe_erase.
-  - by erewrite bool_decide_iff; last apply erase_val_inj_iff.
+  - by erewrite bool_decide_ext; last apply erase_val_inj_iff.
   - by assert (vals_compare_safe (erase_val v1) (erase_val v2))
       by by apply vals_compare_safe_erase.
 Qed.