From 2383b600e9d03a6688aefefb14aa8c5a4fdcfbd6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Nov 2018 00:55:33 +0100
Subject: [PATCH] =?UTF-8?q?Instance=20for=20`Timeless=20(=E2=96=A1=20P)`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/bi/derived_laws_sbi.v b/theories/bi/derived_laws_sbi.v
index e1e93317e..72ba65760 100644
--- a/theories/bi/derived_laws_sbi.v
+++ b/theories/bi/derived_laws_sbi.v
@@ -449,6 +449,10 @@ Proof. rewrite /bi_affinely; apply _. Qed.
 Global Instance absorbingly_timeless P : Timeless P → Timeless (<absorb> P).
 Proof. rewrite /bi_absorbingly; apply _. Qed.
 
+Global Instance intuitionistically_timeless P :
+  Timeless (PROP:=PROP) emp → Timeless P → Timeless (□ P).
+Proof. rewrite /bi_intuitionistically; apply _. Qed.
+
 Global Instance eq_timeless {A : ofeT} (a b : A) :
   Discrete a → Timeless (PROP:=PROP) (a ≡ b).
 Proof. intros. rewrite /Discrete !discrete_eq. apply (timeless _). Qed.
-- 
GitLab