Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
ordinal
(
91630..
(
4ae4a..
4a7ef..
)
)
.
Apply H0 with
False
.
Assume H1:
TransSet
(
91630..
(
4ae4a..
4a7ef..
)
)
.
Assume H2:
∀ x0 .
prim1
x0
(
91630..
(
4ae4a..
4a7ef..
)
)
⟶
TransSet
x0
.
Apply unknownprop_7f22ba84596096506346d841e7ea5fb6e860e1d5c7692fdfdf0f0290abbc64e9.
The subproof is completed by applying H1.
■