From 65171af2369257a330b71aca55e1b96d58a094c0 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Sep 2016 10:43:17 +0200
Subject: [PATCH] Alternative version of ownM_empty.

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

diff --git a/algebra/upred.v b/algebra/upred.v
index 18e438efb..261c727dd 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1257,6 +1257,8 @@ Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
 Proof. by intros; rewrite ownM_valid valid_elim. Qed.
 Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
 Proof. intros a b [b' ->]. rewrite ownM_op. eauto. Qed.
+Lemma ownM_empty' : uPred_ownM ∅ ⊣⊢ True.
+Proof. apply (anti_symm _); auto using ownM_empty. Qed.
 
 (* Viewshifts *)
 Lemma rvs_intro P : P =r=> P.
-- 
GitLab