From 8d55728b66304e6708abc8839dde2e5e1722cd72 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 Feb 2017 12:58:01 +0100
Subject: [PATCH] More constructors for LimitPreserving.

---
 theories/algebra/ofe.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 9f513eea9..dba18011f 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -1081,6 +1081,13 @@ Section limit_preserving.
   (* These are not instances as they will never fire automatically...
      but they can still be helpful in proving things to be limit preserving. *)
 
+  Global Instance limit_preserving_const (P : Prop) : LimitPreserving (λ _, P).
+  Proof. intros c HP. apply (HP 0). Qed.
+
+  Lemma limit_preserving_timeless (P : A → Prop) :
+    Proper (dist 0 ==> impl) P → LimitPreserving P.
+  Proof. intros PH c Hc. by rewrite (conv_compl 0). Qed.
+
   Lemma limit_preserving_and (P1 P2 : A → Prop) :
     LimitPreserving P1 → LimitPreserving P2 →
     LimitPreserving (λ x, P1 x ∧ P2 x).
-- 
GitLab