proposition: Lemma fold_equiv : forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A), fold f s a = fold' f s a.
proof: Proof. unfold fold', elements. simple induction s; simpl; auto; intros. rewrite fold_equiv_aux. rewrite H0. simpl; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int