proposition: Lemma to_cumul_cumulative {X} (L : nat -> list X) : cumulative (to_cumul L).
proof: Proof. eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List