Search for blocks/addresses/...

Proofgold Proof

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