proposition: Lemma fold_spec m {A} (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. rewrite fold_equiv. unfold fold'. now rewrite L.fold_spec. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)