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