proposition: Lemma refine_decides_forall_In' : forall {A} l (P: A -> Prop) (P_Dec : DecideableEnsemble P), refine {b | decides b (forall (x: A), List.In x l -> P x)} {b | decides b (~ exists (x : A), List.In x l /\ ~ P x)}.
proof: Proof. unfold refine; intros; computes_to_inv. computes_to_constructor. destruct v; simpl in *; intros. case_eq (dec x); intros; try rewrite <- (dec_decides_P); eauto. exfalso; eapply H; eexists; intuition eauto. rewrite <- dec_decides_P in H2; congruence. unfold not in *; intros. eapply H; intros. destruct H1; intuition. 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