diff --git a/theories/fin_collections.v b/theories/fin_collections.v
index 72b6c2386f54a5457d96f19eed836d7098c8c000..576bf4fad16690cc10d235b1d88ab765cbb7fa4c 100644
--- a/theories/fin_collections.v
+++ b/theories/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.