proposition: Lemma enumerator_to_list_enumerator : forall x, (exists n, e n = Some x) <-> (exists n, In x (T n)).
proof: Proof. split; intros [n H]. - exists n. unfold T. rewrite H. firstorder. - unfold T in *. destruct (e n) eqn:E. inversion H; subst. eauto. inversion H0. inversion H. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List