proposition: Lemma elements_empty_iff X : elements X = [] ↔ X ≡ ∅.
proof: Proof. rewrite <-Permutation_nil_r. split; [|intros ->; by rewrite elements_empty]. intros HX. apply elem_of_equiv_empty; intros x. rewrite <-elem_of_elements, HX. apply not_elem_of_nil. Qed.
imports: stdpp(relations) stdpp(options)