proposition: Lemma list_enumerator_enumerator {X} {p : X -> Prop} {T} : list_enumerator T p -> enumerator (fun n => let (n, m) := Cantor.of_nat n in nth_error (T n) m) p.
proof: Proof. unfold list_enumerator. intros H x. rewrite list_enumerator_to_enumerator. eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List