From 8b9a96ade73014d9e6c58634ec70276d322dfe42 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 23 Sep 2016 13:58:52 +0200
Subject: [PATCH] Relate "elements" of a finite set to nil.

---
 prelude/fin_collections.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/prelude/fin_collections.v b/prelude/fin_collections.v
index 31738a5d6..0aaf5bd51 100644
--- a/prelude/fin_collections.v
+++ b/prelude/fin_collections.v
@@ -38,6 +38,17 @@ Proof.
   apply elem_of_nil_inv; intros x.
   rewrite elem_of_elements, elem_of_empty; tauto.
 Qed.
+Lemma elements_empty_inv X : elements X = [] → X ≡ ∅.
+Proof.
+  intros HX; apply elem_of_equiv_empty; intros x.
+  rewrite <-elem_of_elements, HX, elem_of_nil. tauto.
+Qed.
+Lemma elements_empty' X : elements X = [] ↔ X ≡ ∅.
+Proof.
+  split; intros HX; [by apply elements_empty_inv|].
+  by rewrite <-Permutation_nil, HX, elements_empty.
+Qed.
+
 Lemma elements_union_singleton (X : C) x :
   x ∉ X → elements ({[ x ]} ∪ X) ≡ₚ x :: elements X.
 Proof.
-- 
GitLab