fact: Definition list_enumerator {X} (L: nat -> list X) (p : X -> Prop) := forall x, p x <-> exists m, In x (L m).
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts EnumerabilityFacts) Undecidability.Shared.Dec List