From 739f63418f2f7a9a5605d7a55c114ec87958c6c2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 21 Jul 2016 11:16:59 +0200
Subject: [PATCH] show that uPred_holds is NE

---
 algebra/upred.v | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 607214971..be93b5991 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -50,12 +50,19 @@ Section cofe.
 End cofe.
 Arguments uPredC : clear implicits.
 
-Instance uPred_ne' {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
+Instance uPred_ne {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
 Proof.
   intros x1 x2 Hx; split=> ?; eapply uPred_mono; eauto; by rewrite Hx.
 Qed.
 Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
-Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.
+Proof. by intros x1 x2 Hx; apply uPred_ne, equiv_dist. Qed.
+
+Lemma uPred_holds_ne {M} (P Q : uPred M) n1 n2 x :
+  P ≡{n2}≡ Q → n2 ≤ n1 → ✓{n2} x → Q n1 x → P n2 x.
+Proof.
+  intros [Hne] ???. eapply Hne; try done.
+  eapply uPred_closed; eauto using cmra_validN_le.
+Qed.
 
 (** functor *)
 Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
-- 
GitLab