Proofgold Proof

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