fact: Definition enum_PA_funcs : nat -> option PA_funcs := (fun k => match k with | 0 => Some Zero | 1 => Some Succ | 2 => Some Plus | _ => Some Mult end).
imports: Undecidability.FOL.Utils.FullSyntax Undecidability.Synthetic(EnumerabilityFacts ListEnumerabilityFacts) List