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