Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
u17
=
u20
.
Apply In_irref with
u17
.
Apply H0 with
λ x0 x1 .
u17
∈
x1
.
The subproof is completed by applying unknownprop_ceb44d185673fa4a0bfe7b9d4c7586adc91021a2759228a04ba38661d3ba0f80.
■