Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: Field x0. Apply unknownprop_d42950c3f12a0a1bd59ad028e6131cf8cd8c077fb27dae2f0fb2adeb65747c62 with x0. Apply Field_is_CRing_with_id with x0. The subproof is completed by applying H0. ■