proposition: Lemma enumerable_semi_decidable {X} {p : X -> Prop} : discrete X -> enumerable p -> semi_decidable p.
proof: Proof. unfold enumerable, enumerator. intros [d Hd] [f Hf]. exists (fun x n => if! f n is Some y then d (x,y) else false). intros x. rewrite Hf. split. - intros [n Hn]. exists n. rewrite Hn. now eapply Hd. - intros [n Hn]. exists n. destruct (f n); inversion Hn. eapply Hd in Hn. now subst. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia