proposition: Lemma filter_join_lists : forall {A B} (f: A * B -> bool) xs ys, filter f (Join_Lists xs ys) = (flat_map (fun x => map (fun y => (x, y)) (filter (fun y : B => f (x, y)) ys)) xs).
proof: Proof. intros. unfold Join_Lists. rewrite filter_flat_map. setoid_rewrite filter_map. reflexivity. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.SetEq Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListMorphisms Fiat.Common.List.FlattenList Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.Common.List.ListFacts