proposition: Lemma list_enumerable_enumerable {X} {p : X -> Prop} : list_enumerable p -> enumerable p.
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