Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_225064cd1bf1585f78cf88aa05e4877722b35dd1efb5b84c02c1437756d86856 with
λ x2 x3 : ι → ι → ο . x3 x0 x1 ⟶ ∀ x4 : ο . (∀ x5 : ι → ι . bij x0 x1 x5 ⟶ x4) ⟶ x4.
Assume H0:
(λ x2 x3 . ∃ x4 : ι → ι . bij x2 x3 x4) x0 x1.
Let x2 of type ο be given.
Assume H1:
∀ x3 : ι → ι . bij x0 x1 x3 ⟶ x2.
Apply H0 with
x2.
The subproof is completed by applying H1.