proposition: Lemma fold_1 : forall 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) (elements m) i.
proof: Proof. induction m as [|[a m]]; intros A i f; simpl; auto. Qed.
imports: FMapInterface