Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_3189570886a432a72e87efcbd0ea995fafcd88c6ec3c7fdffceb2e344a826cdc with
x2,
λ x3 x4 . In x2 (lam x0 (λ x5 . x1 x5)) ⟶ setsum x3 (ap x2 1) = x2.
Apply unknownprop_3030666c70e3b0a40e79c3dea18074452b4f067cae53efb13b5a85e3938a9613 with
x2,
λ x3 x4 . In x2 (lam x0 (λ x5 . x1 x5)) ⟶ setsum (proj0 x2) x3 = x2.
The subproof is completed by applying unknownprop_1006fa3f7c99c66c88f5928e4fedbeb0f7fbd3d083c6fed73e217b8c50a9a235 with x0, λ x3 . x1 x3, x2.