proposition: Theorem dec_count_enum {X} {p : X -> Prop} : decidable p -> enumerable__T X -> enumerable p.
proof: Proof. intros ? % decidable_semi_decidable ?. now eapply semi_decidable_enumerable. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia