Search for blocks/addresses/...
Proofgold Proof
pf
Apply Eps_i_ex with
λ x0 .
∀ x1 .
nIn
x1
x0
.
The subproof is completed by applying unknownprop_aa086d387ad76504b85710f51cf9e33114e595d92e12aa01d2bc3cc165a2a769.
■