Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Apply equip_atleastp with x0, x0.
The subproof is completed by applying equip_ref with x0.