proposition: Lemma cum_ge' {X} {L: nat -> list X} {x n m} : cumulative L -> In x (L n) -> m >= n -> In x (L m).
proof: Proof. intros ? H [A ->] % (cum_ge (L := L)). apply in_app_iff. eauto. eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List