proposition: Lemma enumerable_enum {X} {p : X -> Prop} : enumerable p <-> list_enumerable p.
proof: Proof. split. eapply enumerable_list_enumerable. eapply list_enumerable_enumerable. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts) Undecidability.Shared(Dec) List