Search for blocks/addresses/...
Proofgold Proof
pf
Assume H0:
ordinal
(
Sing
1
)
.
Apply unknownprop_325f2340f4f02c3983f16a931a6d1430c028cf3d83044145e28f6565821b1b7d.
Apply unknownprop_e682831a7124f89af4a1b1d248afbcd452dfbbb9d90b9a88db6885fe36808b65 with
Sing
1
.
The subproof is completed by applying H0.
■