proposition: Lemma fold_union: (forall x, mem x s && mem x s'=false) -> eqA (fold f (union s s') i) (fold f s (fold f s' i)).
proof: Proof. intros; apply fold_union with (eqA:=eqA); auto. intros; rewrite exclusive_set; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx