Search for blocks/addresses/...

Proofgold Proof

pf
Let x0 of type ι be given.
Assume H0: 4a7ef.. = 4ae4a.. x0.
Claim L1: nIn x0 (4ae4a.. x0)
Apply H0 with λ x1 x2 . nIn x0 x1.
The subproof is completed by applying unknownprop_da3368fefc81e401e6446c98c0c04ab87d76d6f97c47fe5fd07c1e3c2f00ef6a with x0.
Apply L1.
The subproof is completed by applying unknownprop_38ce50d6b52a0a920b530e7796207ec902a42d65414467df1ecd3efb123f4cb9 with x0.