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 K_field_4 x0 x0, λ x2 x3 . K_field_2_b x0 x0 x1 x3. ■