Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: CRing_with_id x0. Let x1 of type ι be given. Let x2 of type ι be given. Assume H1: x2 ∈ omega. Apply nat_primrec_S with field4 x0, λ x3 x4 . field2b x0 x1 x4, x2. Apply omega_nat_p with x2. The subproof is completed by applying H1. ■