Apply functional extensionality with
Inj1,
setsum 1.
Let x0 of type ι be given.
Apply unknownprop_cf6cb9ac2ba2b95572013c10cbd74c677c393380327c9f33d6487f09608dd39e with
setsum 1 x0,
Inj1 x0.
The subproof is completed by applying unknownprop_8438e883de7a1eeb39e847b7d0ce5ef143abdad5f0a5010ee69558812716e137 with x0.