From 15fd682e4e8673bf3108c253333221365fde3f9d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 16 May 2022 20:17:20 +0200
Subject: [PATCH] updates preserve being Absorbing

---
 iris/bi/updates.v | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/iris/bi/updates.v b/iris/bi/updates.v
index a26a18352..99b613eaa 100644
--- a/iris/bi/updates.v
+++ b/iris/bi/updates.v
@@ -240,6 +240,10 @@ Section bupd_derived.
     by rewrite -bupd_intro -or_intro_l.
   Qed.
 
+  Global Instance bupd_absorbing P :
+    Absorbing P → Absorbing (|==> P).
+  Proof. rewrite /Absorbing /bi_absorbingly bupd_frame_l =>-> //. Qed.
+
   Section bupd_plainly.
     Context `{!BiPlainly PROP, !BiBUpdPlainly PROP}.
 
@@ -326,6 +330,10 @@ 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.
 
+  Global Instance fupd_absorbing E1 E2 P :
+    Absorbing P → Absorbing (|={E1,E2}=> P).
+  Proof. rewrite /Absorbing /bi_absorbingly fupd_frame_l =>-> //. Qed.
+
   Lemma fupd_trans_frame E1 E2 E3 P Q :
     ((Q ={E2,E3}=∗ emp) ∗ |={E1,E2}=> (Q ∗ P)) ={E1,E3}=∗ P.
   Proof.
-- 
GitLab