Apply unknownprop_abe15cc9bd131c95b0b9585b43caa22ca6fcee57a092fd0cd1b55cd95e75595e with
λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 . In x4 (x0 x2 x3) ⟶ or (∃ x5 . and (In x5 x2) (x4 = x0 0 x5)) (∃ x5 . and (In x5 x3) (x4 = x0 1 x5)).
The subproof is completed by applying unknownprop_c529973cb32f8d02a3950eda53e547d40c4a0e8faca1777353233a3377534f09.