proposition: Lemma cumul_spec {X} {L} {p : X -> Prop} : list_enumerator L p -> list_enumerator (to_cumul L) p.
proof: Proof. unfold list_enumerator. intros. now rewrite <- to_cumul_spec. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List