Search for blocks/addresses/...
Proofgold Proof
pf
Let x0 of type
ι
be given.
Assume H0:
c7ce4..
x0
.
Apply unknownprop_8da13791b7dd1ebf2304410ec45eba97dfe397ef11526a77be93821c0ea7f214 with
x0
,
SNo
(
d634d..
x0
)
leaving 2 subgoals.
The subproof is completed by applying H0.
Assume H1:
SNo
(
d634d..
x0
)
.
Assume H2:
x0
=
ad280..
(
28f8d..
x0
)
(
d634d..
x0
)
.
The subproof is completed by applying H1.
■