Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_2c926b240fc658005337215abfdc8124a6f6eea17ba9f4df80d254bab3845972 with
λ x2 x3 : ι → ι → ο . x3 x0 x1 ⟶ ∀ x4 . In x4 x1 ⟶ ∃ x5 . and (In x5 x0) (∃ x6 . x4 = setsum x5 x6).
Assume H0:
∀ x2 . In x2 x1 ⟶ ∃ x3 . and (In x3 x0) (∃ x4 . x2 = setsum x3 x4).
The subproof is completed by applying H0.