diff --git a/opam b/opam
index 44dc6b5a6a260786435ae69de9f88aaf9f0f457c..1a3c4b01a3845faf9d7f24f1627dcf524cf74059 100644
--- a/opam
+++ b/opam
@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.9~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2018-05-14.0.8fdeb77f") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-05-23.0.a8f65af5") | (= "dev") }
 ]
diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 920ae9a31029dedf850cdf08e236a4733c3dd6a2..6801268688cf11d35e1896a2ca5fde9644c806b1 100644
--- a/theories/algebra/local_updates.v
+++ b/theories/algebra/local_updates.v
@@ -52,6 +52,13 @@ Section updates.
     apply (cancelableN x); first done. by rewrite -cmra_op_opM_assoc.
   Qed.
 
+  Lemma replace_local_update x y `{!IdFree x} :
+    ✓ y → (x, x) ~l~> (y, y).
+  Proof.
+    intros ? n mz ? Heq; simpl in *; split; first by apply cmra_valid_validN.
+    destruct mz as [z|]; [|done]. by destruct (id_freeN_r n n x z).
+  Qed.
+
   Lemma local_update_discrete `{!CmraDiscrete A} (x y x' y' : A) :
     (x,y) ~l~> (x',y') ↔ ∀ mz, ✓ x → x ≡ y ⋅? mz → ✓ x' ∧ x' ≡ y' ⋅? mz.
   Proof.