proposition: Lemma to_cumul_spec {X} (L : nat -> list X) x : (exists n, In x (L n)) <-> exists n, In x (to_cumul L n).
proof: Proof. split. - intros [n H]. exists (S n). cbn. eapply in_app_iff. eauto. - intros [n H]. induction n; cbn in *. + inversion H. + eapply in_app_iff in H as [H | H]; eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List