Proofgold Proof

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