Search for blocks/addresses/...

Proofgold Proof

pf
Apply minus_CSNo_minus_SNo with 0, λ x0 x1 . x1 = 0 leaving 2 subgoals. The subproof is completed by applying SNo_0. The subproof is completed by applying minus_SNo_0. ■