proposition: Lemma refine_IndexedEnsemble_Intersection_Intersection heading : forall P Q R, refine {queriedList : list (@RawTuple heading) | UnIndexedEnsembleListEquivalence (IndexedEnsemble_Intersection (IndexedEnsemble_Intersection P Q) R) queriedList} {queriedList : list (@RawTuple heading) | UnIndexedEnsembleListEquivalence (IndexedEnsemble_Intersection P (fun tup => Q tup /\ R tup)) queriedList}.
proof: Proof. intros. eapply refineEquiv_iff_Pick; unfold pointwise_relation; intuition; eapply UnIndexedEnsembleListEquivalence_Same_set; eauto using IndexedEnsemble_Intersection_And. unfold Same_set, Included, In, IndexedEnsemble_Intersection; intuition eauto. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure