proposition: Lemma fold_left_eqlistA_Proper {A B} {RA : relation A} {RB : relation B} : Proper ((RA ==> RB ==> RA) ==> SetoidList.eqlistA RB ==> RA ==> RA) (@fold_left A B).
proof: Proof. unfold respectful. intros ?? H ls1 ls2 H'. induction H'; simpl; eauto with nocore. Qed.
imports: Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.Sorting.Permutation Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.List.ListFacts Fiat.Common.List.Operations Fiat.Common.List.PermutationFacts Fiat.Common.List.FlattenList