fact: Definition cumulative {X} (L: nat -> list X) := forall n, exists A, L (S n) = L n ++ A.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List