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