proposition: Lemma GetAnswers_add_answers_packet : forall answers (p : packet), (add_answers answers p)!"answers" = List.app (rev answers) p!"answers".
proof: Proof. induction answers. - destruct p as [ ? [ ? [ ? [ ? [ ? [ ? [ ? [ ? [ ? [ ? [? [? ? ] ] ] ] ] ] ] ] ] ] ] ]; simpl; eauto. - destruct p as [ ? [ ? [ ? [ ? [ ? [ ? [ ? [ ? [ ? [ ? [? [? ? ] ] ] ] ] ] ] ] ] ] ] ]; simpl. rewrite IHanswers. unfold add_answer. simpl. rewrite <- List.app_assoc. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.Tactics.CacheStringConstant Fiat.Computation.Decidable Fiat.Computation.IfDec Fiat.Computation.FoldComp Fiat.Computation.FueledFix Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Automation.MasterPlan Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindStringPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Bedrock.Word Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Narcissus.Stores.Cache Fiat.Narcissus.Stores.DomainNameStore Fiat.Narcissus.BinLib.AlignedDomainName Fiat.Narcissus.BinLib.AlignedByteString Fiat.Examples.DnsServer.DecomposeSumField Fiat.Examples.DnsServer.SimpleDnsLemmas Fiat.Examples.DnsServer.DnsAutomation Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema