proposition: Lemma fsupp_bunion B s (rr : B -> relation A) (FIN: set_finite s) (FS: forall x (IN: s x), fsupp (rr x)) : fsupp (bunion s rr).
proof: Proof. unfold fsupp, seq; ins; desf. apply set_finite_bunion; ins. apply FS; done. Qed.
imports: Arith micromega.Lia Setoid Morphisms Wf_nat HahnBase HahnList HahnSets HahnRelationsBasic HahnEquational HahnRewrite HahnDom