Search for blocks/addresses/...

Proofgold Proof

pf
Apply Inj1_pair_1_eq with λ x0 x1 : ι → ι . ∀ x2 x3 x4 . x4x3x0 x4setsum x2 x3.
The subproof is completed by applying Inj1_setsum.