proposition: Lemma list_enumerator_to_enumerator : forall x, (exists n, e n = Some x) <-> (exists n, In x (T n)).
proof: Proof. split; intros [k H]. - unfold e in *. destruct (Cantor.of_nat k) as (n, m). exists n. eapply (nth_error_In _ _ H). - unfold e in *. eapply In_nth_error in H as [m]. exists (Cantor.to_nat (k, m)). now rewrite Cantor.cancel_of_to, H. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List