Apply unknownprop_8583c67a5354a94a214412f684d3146c279871f65a15e5b831f23231b1641441 with
λ x0 x1 : ι → ι . ∀ x2 x3 . In x3 (x1 x2) ⟶ ∃ x4 . and (In x4 x2) (x3 = Inj1 x4).
Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_74e6ddb76e51f556d0e4a910f649c4782bc9cb375d38baef38a8c05a47e8ef22 with
x0,
Inj1,
x1.
The subproof is completed by applying H0.