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