proposition: Lemma fold_spec m : forall (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. induction m as [|(k,e) m IH]; simpl; auto. Qed.
imports: Coq(OrdersFacts OrdersLists)