proposition: Lemma remove_fold_2: mem x s=false -> eqA (fold f (remove x s) i) (fold f s i).
proof: Proof. intros; apply remove_fold_2 with (eqA:=eqA); auto. rewrite not_mem_iff; auto. Qed.
imports: MSetProperties Zerob Sumbool Lia DecidableTypeEx