proposition: Lemma fold_1 m (A : Type) (i : A) (f : key -> elt -> A -> A) : fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (bindings m) i.
proof: Proof. apply fold_spec. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)