proposition: Lemma flatmap_permutation : forall heading l1 (l2 : list (@RawTuple heading)), In _ (FlattenCompList.flatten_CompList (map (fun r : @RawTuple heading => Return r) l2)) l1 -> Permutation l1 l2.
proof: Proof. intros. revert l1 H. induction l2; intros; destruct l1; intros; simpl in *; try reflexivity; inv H; (inv H0; inv H1; inv H0; inv H2; inv H). - inv H3. - rewrite app_singleton. auto. 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