From 1a3f06a61f860162cb92c672bcf98a0b32985c95 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2016 10:36:49 +0100
Subject: [PATCH] prelude.collections: add lemma to prove non-emptiness

---
 theories/collections.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/theories/collections.v b/theories/collections.v
index 93f3493d..f83a8e9c 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -280,6 +280,8 @@ Section collection.
     intros X1 X2 HX Y1 Y2 HY; apply elem_of_equiv; intros x.
     by rewrite !elem_of_difference, HX, HY.
   Qed.
+  Lemma non_empty_inhabited x X : x ∈ X → X ≢ ∅.
+  Proof. solve_elem_of. Qed.
   Lemma intersection_singletons x : ({[x]} : C) ∩ {[x]} ≡ {[x]}.
   Proof. solve_elem_of. Qed.
   Lemma difference_twice X Y : (X ∖ Y) ∖ Y ≡ X ∖ Y.
-- 
GitLab