proposition: Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
proof: Proof. split; [|intros ->; by rewrite size_empty]. intros; apply equiv_empty; intros x; rewrite <-elem_of_elements. by rewrite (nil_length_inv (elements X)), ?elem_of_nil. Qed.
imports: stdpp(relations) stdpp(options)