Search for blocks/addresses/...
Proofgold Proof
pf
Apply ordinal_SNo with
omega
.
The subproof is completed by applying omega_ordinal.
■