proposition: Lemma List_Query_In_Return {n} {ResultT} headings (l : list (ilist2 (n := n) (B := @RawTuple) headings)) (r : ilist2 (B := @RawTuple) headings -> ResultT) : refine (List_Query_In l (fun tup => (Return (r tup))%QuerySpec)) (ret (map r l)).
proof: Proof. unfold List_Query_In; induction l; simpl; eauto. - reflexivity. - setoid_rewrite IHl; unfold Query_Return; simplify with monad laws. reflexivity. 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