proposition: Theorem dec_count_enum' X (p : X -> Prop) : decidable p -> enumerable__T X -> enumerable (fun x => ~ p x).
proof: Proof. intros ? % dec_compl ?. eapply dec_count_enum; eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia