Apply unknownprop_182c04046a079c94ddb7633eb3970f1d6314344011f16a11027ed1ec214739d8 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_25f0736e80681cd44329b5b6c9965a9cf95558c1b85c8430e91be63bfeb5cf39.