From 43ee9e86e2949e02283ca91f888398df7897bf0b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 6 Dec 2017 20:26:19 +0100
Subject: [PATCH] Another absorbing instance for wand.

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

diff --git a/theories/bi/derived_laws.v b/theories/bi/derived_laws.v
index e1a37f268..fd36a646a 100644
--- a/theories/bi/derived_laws.v
+++ b/theories/bi/derived_laws.v
@@ -1623,9 +1623,15 @@ Proof. intros. by rewrite /Absorbing -absorbingly_sep_l absorbing. Qed.
 Global Instance sep_absorbing_r P Q : Absorbing Q → Absorbing (P ∗ Q).
 Proof. intros. by rewrite /Absorbing -absorbingly_sep_r absorbing. Qed.
 
-Global Instance wand_absorbing P Q : Absorbing Q → Absorbing (P -∗ Q).
+Global Instance wand_absorbing_l P Q : Absorbing P → Absorbing (P -∗ Q).
+Proof.
+  intros. rewrite /Absorbing /bi_absorbingly. apply wand_intro_l.
+  by rewrite assoc (sep_elim_l P) wand_elim_r.
+Qed.
+Global Instance wand_absorbing_r P Q : Absorbing Q → Absorbing (P -∗ Q).
 Proof. intros. by rewrite /Absorbing absorbingly_wand !absorbing -absorbingly_intro. Qed.
 
+
 Global Instance absorbingly_absorbing P : Absorbing (bi_absorbingly P).
 Proof. rewrite /bi_absorbingly. apply _. Qed.
 Global Instance plainly_absorbing P : Absorbing (bi_plainly P).
-- 
GitLab