From fc4bc498e5109232ae4f423ef5af4bef5afba2b6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 23 Jul 2023 10:14:31 +0200
Subject: [PATCH] Add lemma `delete_option_local_update_cancelable`.

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

diff --git a/iris/algebra/local_updates.v b/iris/algebra/local_updates.v
index dd679d26f..c8a854745 100644
--- a/iris/algebra/local_updates.v
+++ b/iris/algebra/local_updates.v
@@ -200,3 +200,10 @@ Proof.
   move: Hy. rewrite Heq /= -Some_op=>Hy. eapply Hex.
   eapply cmra_validN_le; [|lia]. eapply Hy.
 Qed.
+
+Lemma delete_option_local_update_cancelable {A : cmra} (mx : option A) :
+  Cancelable mx → (mx, mx) ~l~> (None, None).
+Proof.
+  intros ?. apply local_update_unital=>n mf /= Hmx Heq. split; first done.
+  rewrite left_id. eapply (cancelableN mx); by rewrite right_id_L.
+Qed.
-- 
GitLab