From 81685f698a6e66cf72ce8613e1622d996f7f058a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 9 Mar 2020 18:43:51 +0100
Subject: [PATCH] =?UTF-8?q?Add=20lemma=20`except=5F0=5Finto=5Flater=20P=20?=
 =?UTF-8?q?:=20=E2=97=87=20P=20=E2=8A=A2=20=E2=96=B7=20P`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/derived_laws_sbi.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index 9953ed04b..c7fadbd22 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -385,6 +385,8 @@ Proof.
 Qed.
 Lemma except_0_later P : ◇ ▷ P ⊢ ▷ P.
 Proof. by rewrite /sbi_except_0 -later_or False_or. Qed.
+Lemma except_0_into_later P : ◇ P ⊢ ▷ P.
+Proof. by rewrite -except_0_later -later_intro. Qed.
 Lemma except_0_persistently P : ◇ <pers> P ⊣⊢ <pers> ◇ P.
 Proof.
   by rewrite /sbi_except_0 persistently_or -later_persistently persistently_pure.
-- 
GitLab