proposition: Lemma fold_left_map : forall {A B} f seq, @List.fold_left (list B) A (fun a b => f b :: a) seq [] = List.map f (rev seq).
proof: Proof. intros; rewrite <- fold_left_rev_right; apply fold_right_map. 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