proposition: Lemma prefix_trans : forall b b' b'' : string, prefix b b' -> prefix b' b'' -> prefix b b''.
proof: Proof. induction b; simpl; auto. - destruct b''; simpl; eauto. - induction b'; simpl; intros; intuition eauto. unfold is_true in H; discriminate. find_if_inside; subst. destruct b''; simpl in *. + unfold is_true in *; discriminate. + find_if_inside; subst; eauto. + unfold is_true in *; discriminate. 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