proposition: Lemma refine_List_For_Query_In_Return_Permutation : forall (QueryT ResultT : Type) (l : list QueryT) (proj : QueryT -> ResultT), refine (For (List_Query_In l (fun tup : QueryT => Return (proj tup))))%QuerySpec (Pick (fun l' => Permutation (map proj l) l')).
proof: Proof. intros; rewrite refine_List_Query_In_Return; unfold Query_For; computes_to_econstructor; eauto. 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