proposition: Lemma fold_m_ext f : Proper (E.eq ==> eqA ==> eqA) f -> transpose eqA f -> forall f', feq f f' -> forall s s', s [=] s' -> forall a a', eqA a a' -> eqA (fold f s a) (fold f' s' a').
proof: Proof. intros fm ft f' ff' s s' ss' a a' aa'; revert s' ss' a a' aa'. pattern s; apply set_induction_bis; clear s. intros s s' ss' h t s't a a' aa'. trans (fold f s a). apply fold_equal; auto. hyp. apply h. trans s'; hyp. hyp. intros s' e a a' aa'. trans (fold f' empty a'). rewrite 2!fold_empty. hyp. apply fold_m; try hyp||refl. rewrite <- ff'. hyp. intros x s nxs h s' e a a' aa'. trans (fold f' (add x s) a'). rewrite 2!fold_add; unfold compat_op; try rewrite <- ff'; auto. apply ff'. refl. apply h. refl. hyp. apply fold_m; auto. rewrite <- ff'. hyp. refl. Qed.
imports: Coq(FSets) CoLoR(LogicUtil RelUtil BoolUtil)