Apply functional extensionality with
Inj0,
setsum 0.
Let x0 of type ι be given.
Apply unknownprop_cf6cb9ac2ba2b95572013c10cbd74c677c393380327c9f33d6487f09608dd39e with
setsum 0 x0,
Inj0 x0.
The subproof is completed by applying unknownprop_b91672ef87db9f1f183ca0bec3d177e24552087c0e2239281cc5d11522d85a9b with x0.