fact: Definition fsupp A (r: relation A) := forall y, exists findom, forall x (REL: r x y), In x findom.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom