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