Proofgold Proof

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