proposition: Lemma fsupp_list r (FS: fsupp r) l : exists findom, forall x y (REL: r x y) (IN: In y l), In x findom.
proof: Proof. induction l; ins; desf. by exists nil; ins. specialize (FS a); desf. exists (findom ++ findom0); ins; desf; eauto using in_or_app. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom