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