proposition: Lemma cum_ge {X} {L: nat -> list X} {n m} : cumulative L -> m >= n -> exists A, L m = L n ++ A.
proof: Proof. induction 2 as [|m _ IH]. - exists nil. now rewrite app_nil_r. - destruct (H m) as (A&->), IH as [B ->]. exists (B ++ A). now rewrite app_assoc. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List