proposition: Lemma fold_empty : forall A B C (m:monoid_op C) (f:A->B->C), fold m f (\{}:map A B) = monoid_neutral m.
proof: Proof. Proof using. intros. rewrite fold_eq_fold_pairs. match goal with |- context [ set_st ?X] => cuts_rewrite (set_st X = \{}) end. rewrite~ fold_empty. rew_set. intros [k x]. rew_set. iff (?&?&M&N) ?; tryfalse. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)