proposition: Lemma fold_compat (f : E.t -> bool -> bool) (g : E.t -> bool -> bool) x x' init init' : compat_op E.eq Logic.eq f -> compat_op E.eq Logic.eq g -> Equal x x' -> init = init' -> (forall e acc, In e x -> f e acc = g e acc) -> fold f x init = fold g x' init'.
proof: Proof. revert x' init init'. induction x using set_induction_below. intros x' init init' Hf Hg Hx Hinit Hcompat. rewrite 2 fold_empty; auto with typeclass_instances. rewrite <- Hx. auto. intros x' init init' Hf Hg Hx Hinit Hcompat. rewrite (fold_equal _ Hf _ H1). rewrite H1 in Hx. symmetry in Hx. rewrite (fold_equal _ Hg _ Hx). rewrite 2 fold_add_below; auto with typeclass_instances. apply IHx1. apply Hf. apply Hg. reflexivity. rewrite Hinit. apply Hcompat. rewrite H1. apply add_1. setdec. intros e acc He. apply Hcompat. rewrite H1. setdec. Qed.
imports: Coq(FSets) ATBR(Common) ATBR(BoolView)