proposition: Lemma fold_equiv_aux : forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A) acc, L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a).
proof: Proof. simple induction s. - simpl; intuition. - simpl; intros. rewrite H. simpl. apply H0. Qed.
imports: FunInd FMapInterface FMapList ZArith Int