proposition: Lemma refine_decides_QType_match : forall rType qType, ?[ QType_dec qType CNAME ] = true -> refine {b : bool | decides b (QType_match rType qType)} (ret (if (QType_dec rType CNAME) then true else false)).
proof: Proof. intros ? ?; find_if_inside; intros; try discriminate. subst. refine pick val _; try reflexivity. find_if_inside; subst; simpl. econstructor 2; eauto. intro; inversion H0; subst. compute in H1; discriminate. congruence. 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