proposition: Lemma enumerator_PA_preds : enumerator__T enum_PA_preds PA_preds.
proof: Proof. intros []. now exists 0. Qed.
imports: Undecidability.FOL.Utils.FullSyntax Undecidability.Synthetic(EnumerabilityFacts ListEnumerabilityFacts) List