proposition: Lemma In_cumul {X} (L : nat -> list X) x n : In x (to_cumul L n) -> exists n, In x (L n).
proof: Proof. intros H. eapply to_cumul_spec. eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List