proposition: Lemma flatten_Complist_app {A} : forall (l : list (Comp (list A))) l' l'', (forall a v, List.In a l -> computes_to a v -> (exists a', v = [a']) \/ v = nil) -> FlattenCompList.flatten_CompList l ↝ l' ++ l'' -> exists l3 l4, FlattenCompList.flatten_CompList l3 ↝ l' /\ FlattenCompList.flatten_CompList l4 ↝ l'' /\ l = l3 ++ l4.
proof: Proof. induction l; simpl; intros; computes_to_inv; subst. - symmetry in H0; eapply app_eq_nil in H0; intuition; subst. eexists nil, nil; simpl; intuition eauto. - destruct (fun G => H _ _ G H0); destruct_ex; intuition; subst. + simpl in H0''; destruct l'; simpl in H0''; subst. eexists nil, (a :: l); simpl; intuition eauto. injections. apply IHl in H0'; destruct_ex; intuition eauto; subst. eexists (_ :: _), _; simpl; intuition eauto. + simpl in H0''; subst. apply IHl in H0'; destruct_ex; intuition eauto; subst. eexists (_ :: _), _; simpl; intuition 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