proposition: Lemma fold_1 : forall s (A : Type) (eqA : A -> A -> Prop) (st : Equivalence eqA) (i : A) (f : elt -> A -> A), Empty s -> eqA (fold f s i) i.
proof: Proof. unfold Empty; intros; destruct (fold_0 s i f) as (l,(H1, (H2, H3))). rewrite H3; clear H3. generalize H H2; clear H H2; case l; simpl; intros. - reflexivity. - elim (H e). elim (H2 e); intuition. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide