proposition: Theorem fold_rec_bis' : forall (i:A)(s:t), (forall s s' a a', s[=]s' -> eqA a a' -> P s a -> P s' a') -> (P empty i ) -> (forall x a s', In x s -> ~In x s' -> P s' a -> P (add x s') (f x a)) -> P s (fold f s i).
proof: Proof. intros i . induction s using set_induction_above. intros Hc HA _. eapply Hc; eauto. symmetry. auto. rewrite fold_empty. reflexivity. auto. intros Hs HA Hrec. eapply Hs. symmetry; eauto. symmetry. rewrite (fold_equal equivalence_eqA Hcompat _ H1). rewrite fold_add_above. reflexivity. auto. auto. apply Hrec. rewrite H1. setdec. auto. apply IHs1. auto. auto. intros. apply Hrec. rewrite H1. setdec. auto. auto. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)