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.
■