proposition: Lemma set_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
proof: Proof. destruct (elements X) as [|x l] eqn:HX; [right|left]. - apply equiv_empty; intros x. by rewrite <-elem_of_elements, HX, elem_of_nil. - exists x. rewrite <-elem_of_elements, HX. by left. Qed.
imports: stdpp(relations) stdpp(options)