proposition: Lemma fold_rec_weak : forall (A:Type)(P : t -> A -> Type)(f : elt -> A -> A)(i:A), (forall s s' a, s[=]s' -> P s a -> P s' a) -> P empty i -> (forall x a s, ~In x s -> P s a -> P (add x s) (f x a)) -> forall s, P s (fold f s i).
proof: Proof. intros; apply fold_rec_bis; auto. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide