From 24b3e4762bac462368ec6d4a2aaf86ae0886b01b Mon Sep 17 00:00:00 2001
From: Jan-Oliver Kaiser <janno@mpi-sws.org>
Date: Wed, 3 Jun 2015 18:00:05 +0200
Subject: [PATCH] proved timeless_impl

---
 iris_core.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/iris_core.v b/iris_core.v
index 2d7cc373a..89aa27784 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -655,6 +655,16 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
       simpl. eapply HTP; done.
     Qed.
 
+    Lemma timeless_impl P Q:
+      timeless Q ⊑ timeless (P → Q).
+    Proof.
+      move=>w n HTQ /= w' k Ltk HPQ w'' [|[|m]] Lem HP; first exact: bpred.
+      { apply HPQ, HP. omega. }
+      eapply HTQ, HPQ; [omega|omega|].
+      eapply dpred, HP. omega.
+    Qed.
+
+
     Section TimelessQuant.
       Context {T} `{cT : cmetric T}.
       Context (φ : T -n> Props).
-- 
GitLab