Apply unknownprop_24d3fab8c5f2be313e198261133fcc4de3913b4e3dd8f154e7592564c2e0ab41 with
λ x0 x1 : ι → ο . x1 (Inj0 (Power 0)).
Let x0 of type ι → ο be given.
Assume H2:
∀ x1 x2 . x0 x1 ⟶ x0 x2 ⟶ x0 (Inj1 (setsum x1 x2)).
The subproof is completed by applying H1.