proposition: Lemma semi_decider_enumerator {X} {p : X -> Prop} {e f} : enumerator__T e X -> semi_decider f p -> {g | enumerator g p}.
proof: Proof. unfold semi_decider. intros He Hf. exists (fun p => let (n, m) := Cantor.of_nat p in if! e n is Some x then if f x m then Some x else None else None). intros x. rewrite Hf. split. - intros [n Hn]. destruct (He x) as [m Hm]. exists (Cantor.to_nat (m,n)). now rewrite Cantor.cancel_of_to, Hm, Hn. - intros [mn Hmn]. destruct (Cantor.of_nat mn) as (m, n). destruct (e m) as [x'|]; try congruence. destruct (f x' n) eqn:E; inversion Hmn. subst. exists n. exact E. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia