Apply unknownprop_e88b17fc7534a834a3292f38867e04234c9b0d119c42f884c32fbabae05b0d7e with
λ x0 x1 : ι → ι . ∀ x2 x3 x4 . In x4 x3 ⟶ In (x0 x4) (setsum x2 x3).
The subproof is completed by applying unknownprop_509aadde20bd8e655e679e36fea278577d08a1dbe475eed73f3fccc8c2d65f15.