proposition: Lemma flatmap_permutation' : forall heading (l : list (@RawTuple heading)), In _ (@FlattenCompList.flatten_CompList (@RawTuple heading) (@map (@RawTuple heading) (Comp (list (@RawTuple heading))) (fun r : @RawTuple heading => @Query_Return (@RawTuple heading) r) l)) l.
proof: Proof. intros. induction l; simpl. Transparent ret. - unfold ret. apply In_singleton. - Transparent Bind. unfold Bind in *. unfold In in *. eexists. split. * unfold Query_Return in *. unfold ret. apply In_singleton. * exists l. split. + auto. + unfold ret. rewrite app_singleton. apply In_singleton. Opaque ret. Opaque Bind. Qed.
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector Coq.Lists.List Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema