proposition: Lemma eqv_empty A : ⦗@set_empty A⦘ ≡ ∅₂.
proof: Proof. autounfold with unfolderDb; intuition; desf; eauto. Qed.
imports: Program.Basics Arith micromega.Lia Permutation List Setoid HahnBase HahnList HahnRelationsBasic HahnSets