Apply unknownprop_abe15cc9bd131c95b0b9585b43caa22ca6fcee57a092fd0cd1b55cd95e75595e with
λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 x5 . x0 x2 x3 = x0 x4 x5 ⟶ and (x2 = x4) (x3 = x5).
The subproof is completed by applying unknownprop_fafba38828754510d238125ccabe4414010fab04b5feedcfb4fb3ed8bfbb804e.