proposition: Lemma fsupp_eqv (d : A -> Prop) : fsupp ⦗d⦘.
proof: Proof. unfolder; ins; exists (y :: nil); ins; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom