Search for blocks/addresses/...

Proofgold Proof

pf
Apply OSNo_proj1_2 with 0, 1 leaving 2 subgoals. The subproof is completed by applying HSNo_0. The subproof is completed by applying HSNo_1. ■