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.
■