Proofgold Proof

pf
Apply functional extensionality with Inj1, setsum 1. Let x0 of type ι be given. Let x1 of type ι → ι → ο be given. The subproof is completed by applying Inj1_setsum_1L with x0, λ x2 x3 . x1 x3 x2. ■