From 3e8910d930bb82c6fed577b17a764065d825571b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 23 Nov 2022 19:08:34 +0100
Subject: [PATCH] add limit_preserving_emp_valid

---
 iris/bi/derived_laws.v | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/iris/bi/derived_laws.v b/iris/bi/derived_laws.v
index 01af4478a..9af410500 100644
--- a/iris/bi/derived_laws.v
+++ b/iris/bi/derived_laws.v
@@ -1708,6 +1708,11 @@ Proof.
   intros HΦ HΨ c Hc. apply entails_eq_True, equiv_dist=>n.
   rewrite conv_compl. apply equiv_dist, entails_eq_True. done.
 Qed.
+Lemma limit_preserving_emp_valid {A : ofe} `{!Cofe A} (Φ : A → PROP) :
+  NonExpansive Φ → LimitPreserving (λ x, ⊢ Φ x).
+Proof.
+  intros. apply limit_preserving_entails; first solve_proper. done.
+Qed.
 Lemma limit_preserving_equiv {A : ofe} `{!Cofe A} (Φ Ψ : A → PROP) :
   NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊣⊢ Ψ x).
 Proof.
-- 
GitLab