proposition: Lemma semi_decidable_enumerable {X} {p : X -> Prop} : enumerable__T X -> semi_decidable p -> enumerable p.
proof: Proof. intros [e He] [f Hf]. destruct (semi_decider_enumerator He Hf) as [g Hg]. now exists g. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia