proposition: Lemma fold_eq_fold_to_list : forall A B (m:monoid_op B) (f:A->B) (E: set A), fold m f E = LibList.fold m f (to_list E).
proof: Proof. Proof using. reflexivity. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibList LibOperation LibMonoid LibInt LibNat LibEpsilon LibRelation LibMin)