proposition: Lemma enumerator_PA_funcs : enumerator__T enum_PA_funcs PA_funcs.
proof: Proof. intros []. + now exists 0. + now exists 1. + now exists 2. + now exists 3. Qed.
imports: Undecidability.FOL.Utils.FullSyntax Undecidability.Synthetic(EnumerabilityFacts ListEnumerabilityFacts) List