proposition: Lemma fold_over_Values : forall {TValue TAcc} (m: t TValue) f g (init: TAcc), (forall k v acc, f k v acc = g acc v) -> fold f m init = fold_left g (Values m) init.
proof: Proof. intros * equiv. rewrite fold_1. unfold Values. rewrite <- fold_map. revert init; induction (elements m); simpl; eauto. intros; rewrite IHl, equiv; reflexivity. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances