fact: Definition to_cumul {X} (L : nat -> list X) := fix f n := match n with 0 => [] | S n => f n ++ L n end.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List