Proofgold Proof

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