proposition: Lemma fold_single : forall A B C (m:monoid_op C) (f:A->B->C) (k:A) (x:B), Monoid m -> fold m f (k\:=x) = f k x.
proof: Proof. Proof using. intros. rewrite fold_eq_fold_pairs. match goal with |- context [ set_st ?X] => cuts_rewrite (set_st X = \{(k,x)}) end. rewrite~ fold_single. rew_set. intros [k' x']. rew_set. iff (?&?&E&R) M. inverts E. hnf in R. simpls. unfolds single_bind_impl. case_if~. inverts~ R. subst~. inverts M. unfolds binds_impl. simpls. unfolds single_bind_impl. exists k x. splits~. case_if~. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)