proposition: Lemma set_nonemptyE s : ~ s ≡₁ ∅ <-> exists x, s x.
proof: Proof. u; intuition; firstorder. apply NNPP; intro; apply H0; ins; eauto. Qed.
imports: HahnBase Program.Basics List Arith micromega.Lia Relations Setoid Morphisms