proposition: Lemma list_enumerable__T_enumerable {X} : list_enumerable__T X -> enumerable__T X.
proof: Proof. intros [T HT]. eexists. unfold list_enumerator. intros x. rewrite list_enumerator_to_enumerator. eapply HT. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List