proposition: Lemma tuples_in_relation_satisfy_constraint_specific : forall (a : list RawTuple) name (r_n : QueryStructure DnsSchema), For (r in r_n!sRRecords) (Where (prefix r!sNAME name) Return r ) ↝ a -> forall (t t' : resourceRecord) (n0 n' : nat), n0 <> n' -> nth_error a n0 = Some t -> nth_error a n' = Some t' -> get_name t = get_name t' -> RDataTypeToRRecordType t!sRDATA <> CNAME.
proof: Proof. intros. eapply (@tuples_in_relation_satisfy_constraint DnsSchema) in H; try eassumption. simpl in *; intuition. apply DecideableEnsemble_bool. 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