Proofgold Proof

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