Search for blocks/addresses/...

Proofgold Proof

pf
Apply Inj0_setsum_0L with 0, λ x0 x1 . x1 = 0.
The subproof is completed by applying Inj0_0.