From 4e59a653e97854c2be88a675a82dba4ce7b4f39c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 30 Aug 2016 21:55:47 +0200
Subject: [PATCH] Remove ownM_something.

It is unused, and ownM_empty is stronger.
---
 algebra/upred.v | 2 --
 1 file changed, 2 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index eb915a013..07b18ea87 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1128,8 +1128,6 @@ Proof.
   split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
   rewrite -(persistent_core a). by apply cmra_core_monoN.
 Qed.
-Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
-Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
 Lemma ownM_empty : True ⊢ uPred_ownM ∅.
 Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
 
-- 
GitLab