proposition: Lemma enumerator__T_list {X} L : list_enumerator__T L X -> list_enumerator__T (L_list L) (list X).
proof: Proof. intros H l. induction l. - exists 0. cbn. eauto. - destruct IHl as [n IH]. destruct (cumul_spec__T H a) as [m ?]. exists (1 + n + m). cbn. intros. apply in_app_iff. right. apply (in_map (fun '(x, L) => x :: L) _ (a, l)). apply in_prod. all: eapply cum_ge'; eauto using L_list_cumulative; lia. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List