Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: CRing_with_id x0. Let x1 of type ι be given. The subproof is completed by applying nat_primrec_0 with field4 x0, λ x2 x3 . field2b x0 x1 x3. ■