proposition: Lemma Permutation_flatten_CompList {A B} : forall (l l' : list A) (f : A -> Comp (list B)), Permutation l l' -> forall x, FlattenCompList.flatten_CompList (map f l) ↝ x -> exists x', FlattenCompList.flatten_CompList (map f l') ↝ x' /\ Permutation x x'.
proof: Proof. intros ? ? ? H; induction H; simpl; intros; computes_to_inv; subst; eauto. - eapply IHPermutation in H0'; destruct_ex; intuition eauto. eexists; split. computes_to_econstructor; eauto. rewrite H3; reflexivity. - eexists; split. computes_to_econstructor; eauto. rewrite List.app_assoc. rewrite Permutation_app with (l := v ++ v1) (m := v2) (m' := v2). 2: rewrite Permutation_app_comm; reflexivity. rewrite List.app_assoc; reflexivity. reflexivity. - apply IHPermutation1 in H1. destruct_ex; intuition eauto. apply IHPermutation2 in H2; eauto. destruct_ex; intuition eauto. eexists; split; eauto. rewrite H3; eauto. 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