proposition: Lemma cumul_spec__T {X} {L} : list_enumerator__T L X -> list_enumerator__T (to_cumul L) X.
proof: Proof. unfold list_enumerator__T. intros. now rewrite <- to_cumul_spec. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List