From e914cc7efbace0f1a653a113b00d8ee00706dfab Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 23 May 2018 21:30:07 +0200
Subject: [PATCH] Local update `(x, x) ~l~> (y, y)`.

---
 theories/algebra/local_updates.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/algebra/local_updates.v b/theories/algebra/local_updates.v
index 920ae9a31..680126868 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.
-- 
GitLab