Search for blocks/addresses/...

Proofgold Proof

pf
Apply ordinal_SNoLev with 0.
The subproof is completed by applying ordinal_Empty.