proposition: Lemma app_build_FilteredList {A} : forall (l' l'' k' k'' : list A) P, (⟦element in l' | P element ⟧) ↝ k' -> (⟦element in l'' | P element ⟧) ↝ k'' -> (⟦element in l' ++ l'' | P element ⟧) ↝ (k' ++ k'').
proof: Proof. induction l'; simpl; intros; computes_to_inv; subst. - eauto. - computes_to_inv; subst; computes_to_econstructor; eauto. refine pick val v0; simpl; eauto. apply refine_bind_unit; eauto. destruct v0; simpl in *; computes_to_inv; subst; simpl; 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