From d924794587d59d3d02dda214bbc1fc284efea3b0 Mon Sep 17 00:00:00 2001
From: Jonas Kastberg Hinrichsen <jihgfee@gmail.com>
Date: Wed, 9 Nov 2022 11:10:42 +0100
Subject: [PATCH] Added [cmra_update_included] lemma

---
 iris/algebra/updates.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 9807071ce..1f5401ff8 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -107,6 +107,9 @@ Proof. intros n mz. rewrite comm cmra_op_opM_assoc. apply cmra_validN_op_r. Qed.
 Lemma cmra_update_op_r x y : x â‹… y ~~> y.
 Proof. rewrite comm. apply cmra_update_op_l. Qed.
 
+Lemma cmra_update_included x y : x ≼ y → y ~~> x.
+Proof. intros [z ->]. apply cmra_update_op_l. Qed.
+
 Lemma cmra_update_valid0 x y : (✓{0} x → x ~~> y) → x ~~> y.
 Proof.
   intros H n mz Hmz. apply H, Hmz.
-- 
GitLab