proposition: Lemma enumerable_PA_funcs : enumerable__T PA_funcs.
proof: Proof. cbn. exists enum_PA_funcs. apply enumerator_PA_funcs. Qed.
imports: Undecidability.FOL.Utils.FullSyntax Undecidability.Synthetic(EnumerabilityFacts ListEnumerabilityFacts) List