Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: Field x0. Apply explicit_Field_plus_cancelL with field0 x0, field3 x0, field4 x0, field1b x0, field2b x0. Apply Field_explicit_Field with x0. The subproof is completed by applying H0. ■