proposition: Lemma Permuation_filter_flatten {A B} : forall (f : B -> bool) f' l, Permutation (flatten (List.map (fun x : A => List.filter f (f' x)) l)) (List.filter f (flatten (List.map f' l))).
proof: Proof. induction l; simpl. constructor. rewrite filter_app, IHl; reflexivity. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.Arith.PeanoNat Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts