Search for blocks/addresses/...

Proofgold Proof

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