Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
ordinal
(
Sing
2
)
.
Apply H0 with
False
.
Assume H1:
TransSet
(
Sing
2
)
.
Assume H2:
∀ x0 .
x0
∈
Sing
2
⟶
TransSet
x0
.
Apply unknownprop_c1b6591d5fe7667f4ae8b37e57c15660d3c99e820fd43fc7e7d06dca4c9d1c82.
The subproof is completed by applying H1.
■