proposition: Lemma fold_2 : forall s s' x (A : Type) (eqA : A -> A -> Prop) (st : Equivalence eqA) (i : A) (f : elt -> A -> A), compat_op E.eq eqA f -> transpose eqA f -> ~ In x s -> Add x s s' -> eqA (fold f s' i) (f x (fold f s i)).
proof: Proof. intros; destruct (fold_0 s i f) as (l,(Hl, (Hl1, Hl2))); destruct (fold_0 s' i f) as (l',(Hl', (Hl'1, Hl'2))). rewrite Hl2; rewrite Hl'2; clear Hl2 Hl'2. apply fold_right_add with (eqA:=E.eq)(eqB:=eqA). { auto with typeclass_instances. } 1-5: auto. - rewrite <- Hl1; auto. - intros a; rewrite InA_cons; rewrite <- Hl1; rewrite <- Hl'1; rewrite (H2 a); intuition. Qed.
imports: FSetInterface PeanoNat DecidableTypeEx FSetFacts FSetDecide