Search for blocks/addresses/...

Proofgold Proof

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