proposition: Lemma fold_1 : forall (s : t) (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (fun a e => f e a) (elements s) i.
proof: Proof. intros; unfold fold; case (M.fold f s i); unfold elements in *; destruct (M.elements s); auto. Qed.
imports: FSetInterface