proposition: Lemma map_fold : forall {A B TValue} f g m init, (@List.map A B g (fold (fun k (v: TValue) acc => f k v :: acc) m init)) = (fold (fun k v acc => g (f k v) :: acc) m (List.map g init)).
proof: Proof. intros until m; setoid_rewrite fold_1. setoid_rewrite <- fold_left_rev_right; simpl. induction (elements m) as [ | ? ? IH ]; simpl; trivial. setoid_rewrite fold_right_app. setoid_rewrite IH; simpl. 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