Search for blocks/addresses/...

Proofgold Proof

pf
Apply Eps_i_ex with λ x0 . ∀ x1 . iff (prim1 x1 x0) (ba9d8.. x1).
The subproof is completed by applying unknownprop_85e1b59dd4c67fe33ad8d09c2099744e604f5c0327786c73150ce57f2b41b217.