proposition: Lemma enumerable_list_enumerable {X} {p : X -> Prop} : enumerable p -> list_enumerable p.
proof: Proof. intros [f Hf]. eexists. unfold list_enumerator. intros x. rewrite <- enumerator_to_list_enumerator. eapply Hf. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List