proposition: Lemma snd_fold_right {A B A'} (f : B -> A * A' -> A) (g : B -> A' -> A') a a' ls : snd (fold_right (fun b aa' => (f b aa', g b (snd aa'))) (a, a') ls) = fold_right g a' ls.
proof: Proof. induction ls; simpl; trivial. rewrite IHls; reflexivity. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.PeanoNat Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts