proposition: Lemma enumerable_PA_preds : enumerable__T PA_preds.
proof: Proof. exists enum_PA_preds. apply enumerator_PA_preds. Qed.
imports: Undecidability.FOL.Utils.FullSyntax Undecidability.Synthetic(EnumerabilityFacts ListEnumerabilityFacts) List