fact: Definition Join_Comp_Lists {n} {A : Type} {f : A -> Type} {As : Vector.t A n} {a : A} (l' : list (ilist2 (B := f) As)) (c : ilist2 (B := f) As -> Comp (list (f a))) : Comp (list (ilist2 (B := f) (Vector.cons _ a _ As))) := flatten_CompList (map (fun l' => l <- c l'; ret (map (fun fa => icons2 fa l') l)) l').
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