Search for blocks/addresses/...

Proofgold Proof

pf
Apply ordinal_In_SNoLt with 4, 1 leaving 2 subgoals. Apply nat_p_ordinal with 4. The subproof is completed by applying nat_4. The subproof is completed by applying In_1_4. ■