From c46bb2a06e17496b2560eabf886dab8cb412ae6d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 23 Jul 2016 01:22:12 +0200
Subject: [PATCH] Version of fresh using an existential.

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

diff --git a/prelude/collections.v b/prelude/collections.v
index 8391a58d6..98a1a93ef 100644
--- a/prelude/collections.v
+++ b/prelude/collections.v
@@ -807,6 +807,8 @@ Section fresh.
     apply IH. by rewrite E.
   Qed.
 
+  Lemma exist_fresh X : ∃ x, x ∉ X.
+  Proof. exists (fresh X). apply is_fresh. Qed.
   Lemma Forall_fresh_NoDup X xs : Forall_fresh X xs → NoDup xs.
   Proof. induction 1; by constructor. Qed.
   Lemma Forall_fresh_elem_of X xs x : Forall_fresh X xs → x ∈ xs → x ∉ X.
-- 
GitLab