Relate included on uPred to entails.

2308bb5c · Robbert Krebbers · 48d958f2 · 2308bb5c
Commit 2308bb5c authored Sep 28, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 3 additions and 0 deletions

algebra/upred.v algebra/upred.v +3 -0

No files found.
--- 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.