Search for blocks/addresses/...

Proofgold Proof

pf
Apply Inj0_pair_0_eq with λ x0 x1 : ι → ι . ∀ x2 x3 x4 . x4x2x0 x4setsum x2 x3.
The subproof is completed by applying Inj0_setsum.