proposition: Lemma enumerable_list {X} : list_enumerable__T X -> list_enumerable__T (list X).
proof: Proof. intros [L H]. eexists. now eapply enumerator__T_list. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List