proposition: Lemma fold_1 : forall (A:Type)(m:t A)(B:Type)(i : B) (f : key -> A -> B -> B), fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
proof: Proof. intros; unfold fold, elements. rewrite xfoldi_1; reflexivity. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface