proposition: Lemma fold_0 : forall s (A : Type) (i : A) (f : elt -> A -> A), exists l : list elt, NoDup l /\ (forall x : elt, In x s <-> InA x l) /\ fold f s i = fold_right f i l.
proof: Proof. intros; exists (rev (elements s)); split. - apply NoDupA_rev. + auto with typeclass_instances. + auto with set. - split; intros. + rewrite elements_iff; do 2 rewrite InA_alt. split; destruct 1; generalize (In_rev (elements s) x0); exists x0; intuition. + apply fold_spec_right. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide