From 0a5ee4f43e91fe8e36586a3fddd0279402c7d430 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. --- theories/collections.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/collections.v b/theories/collections.v index 88daad82..db4d470e 100644 --- a/theories/collections.v +++ b/theories/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