proposition: Lemma fold_Equal_acc_ : forall {TValue TAcc} {eqA: TAcc -> TAcc -> Prop} {m1 : t TValue} {f} {init init': TAcc}, eqA init init' -> Equivalence eqA -> Proper (E.eq ==> eq ==> eqA ==> eqA) f -> transpose_neqkey eqA f -> eqA (fold f m1 init) (fold f m1 init').
proof: Proof. intros. rewrite (@fold_Equal _ _ eqA); eauto; try reflexivity; []. rewrite !fold_1. generalize H1 H2 init init' H; clear. induction (elements m1); simpl; intros; eauto. eapply IHl; eauto. eapply H1; eauto. Qed.
imports: Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Program.Program Coq.Structures.OrderedTypeEx Fiat.Common Fiat.Common.SetEq Fiat.Common.SetEqProperties Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.LogicFacts Fiat.Common.SetoidClassInstances