proposition: Lemma fold_1 : forall (s:t elt)(Hs:bst s)(A : Type)(i:A)(f : key -> elt -> A -> A), fold f s i = fold_left (fun a p => f p#1 p#2 a) (elements s) i.
proof: Proof. intros. rewrite fold_equiv. unfold fold'. rewrite L.fold_1. unfold L.elements; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int