From 2308bb5ca715a2571a032a8cc1527bdbd7ec0520 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 28 Sep 2016 10:11:39 +0200
Subject: [PATCH] Relate included on uPred to entails.

---
 algebra/upred.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/algebra/upred.v b/algebra/upred.v
index 5083b9d75..d41a5adec 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1513,6 +1513,9 @@ Section cmra.
     eapply uPred_mono with x1; eauto using cmra_includedN_l.
   Qed.
 
+  Lemma uPred_included P Q : P ≼ Q → Q ⊢ P.
+  Proof. intros [P' ->]. apply uPred.sep_elim_l. Qed.
+
   Definition uPred_cmra_mixin : CMRAMixin (uPred M).
   Proof.
     apply cmra_total_mixin; try apply _ || by eauto.
-- 
GitLab