From c148ac4df225e6ea3d830fb3ccd6383d732dfda0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Oct 2018 08:57:11 +0200
Subject: [PATCH] =?UTF-8?q?Prove=20`E2=20=E2=8A=86=20E1=20=E2=86=92=20P=20?=
 =?UTF-8?q?=3D{E1,E2}=3D=E2=88=97=20P`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/updates.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index f36e712e1..480faeda6 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -203,6 +203,13 @@ Section fupd_derived.
   Lemma fupd_wand_r E1 E2 P Q : (|={E1,E2}=> P) ∗ (P -∗ Q) ={E1,E2}=∗ Q.
   Proof. by rewrite fupd_frame_r wand_elim_r. Qed.
 
+  Lemma fupd_mask_weaken E1 E2 P `{!Absorbing P} : E2 ⊆ E1 → P ={E1,E2}=∗ P.
+  Proof.
+    intros ?. rewrite -{1}(right_id emp%I bi_sep P%I).
+    rewrite (fupd_intro_mask E1 E2 emp%I) //.
+    by rewrite fupd_frame_l sep_elim_l.
+  Qed.
+
   Lemma fupd_trans_frame E1 E2 E3 P Q :
     ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P.
   Proof.
-- 
GitLab