Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_24d3fab8c5f2be313e198261133fcc4de3913b4e3dd8f154e7592564c2e0ab41 with
λ x2 x3 : ι → ο . x3 x0 ⟶ x3 x1 ⟶ x3 ((λ x4 x5 . Inj1 (setsum x4 x5)) x0 x1).
Assume H0:
(λ x2 . ∀ x3 : ι → ο . x3 (Inj0 0) ⟶ x3 (Inj0 (Power 0)) ⟶ (∀ x4 x5 . x3 x4 ⟶ x3 x5 ⟶ x3 (Inj1 (setsum x4 x5))) ⟶ x3 x2) x0.
Assume H1:
(λ x2 . ∀ x3 : ι → ο . x3 (Inj0 0) ⟶ x3 (Inj0 (Power 0)) ⟶ (∀ x4 x5 . x3 x4 ⟶ x3 x5 ⟶ x3 (Inj1 (setsum x4 x5))) ⟶ x3 x2) x1.
Let x2 of type ι → ο be given.
Assume H4:
∀ x3 x4 . x2 x3 ⟶ x2 x4 ⟶ x2 (Inj1 (setsum x3 x4)).
Apply H4 with
x0,
x1 leaving 2 subgoals.
Apply H0 with
x2 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.
Apply H1 with
x2 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H4.