proposition: Lemma refine_flatten_CompList_func {A B} : forall (l : list A) (f f' : A -> Comp (list B)), pointwise_relation _ refine f f' -> refine (flatten_CompList (map f l)) (flatten_CompList (map f' l)).
proof: Proof. induction l; simpl; intros. + reflexivity. + rewrite H; setoid_rewrite (IHl f f' H). 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