proposition: Lemma fsupp_restr_eq B (f : A -> B) r : fsupp r -> fsupp (restr_eq_rel f r).
proof: Proof. unfold fsupp, restr_eq_rel; ins; desf. specialize (H y); desf. exists findom; ins; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom