Apply unknownprop_abe15cc9bd131c95b0b9585b43caa22ca6fcee57a092fd0cd1b55cd95e75595e with
λ x0 x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 . In x4 x2 ⟶ ∀ x5 . In x5 (x3 x4) ⟶ In (x0 x4 x5) (lam x2 (λ x6 . x3 x6)).
The subproof is completed by applying unknownprop_1633a25a08ee627a1613041ad1ebe0a4535d0c6ce109cb609e7d9a519dad2f25.