proposition: Lemma filter_join_snd : forall {A B} f s1 s2, List.filter (fun x => f (snd x)) (@Join_Lists A B s1 s2) = Join_Lists s1 (List.filter f s2).
proof: Proof. unfold Join_Lists; induction s2; intros; simpl. - rewrite !flat_map_empty; reflexivity. - rewrite !flat_map_flatten, !flatten_filter in IHs2 |- *. induction s1; simpl in *; trivial. destruct (f a) eqn:eq_fa; simpl in *. f_equal. rewrite IHs1. rewrite filter_map; reflexivity. rewrite <- !flat_map_flatten. apply filter_flat_map_join_snd. rewrite IHs1. rewrite filter_map. simpl; reflexivity. rewrite <- !flat_map_flatten. apply filter_flat_map_join_snd. 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