Apply unknownprop_74210cc9b2960bdcb3eab56d0b4f5ba5a5771478f68cd794d919dafbcd157b00 with
λ x0 x1 : ι → ι . ∀ x2 x3 x4 . In x4 (setsum x2 x3) ⟶ or (∃ x5 . and (In x5 x2) (x4 = x0 x5)) (∃ x5 . and (In x5 x3) (x4 = setsum 1 x5)).
Apply unknownprop_e88b17fc7534a834a3292f38867e04234c9b0d119c42f884c32fbabae05b0d7e with
λ x0 x1 : ι → ι . ∀ x2 x3 x4 . In x4 (setsum x2 x3) ⟶ or (∃ x5 . and (In x5 x2) (x4 = Inj0 x5)) (∃ x5 . and (In x5 x3) (x4 = x0 x5)).
The subproof is completed by applying unknownprop_7d032697ca40cddbc051c2380c77c6793240c9afe41b60a5fed4aabdd07b91ac.