Search for blocks/addresses/...

Proofgold Proof

pf
Apply SNoCutP_SNoCut_lim with omega leaving 2 subgoals. The subproof is completed by applying omega_ordinal. The subproof is completed by applying omega_ordsucc. ■