Apply unknownprop_182c04046a079c94ddb7633eb3970f1d6314344011f16a11027ed1ec214739d8 with
λ x0 x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 . prim1 x4 (0fc90.. x2 (λ x5 . x3 x5)) ⟶ ∃ x5 . and (prim1 x5 x2) (∃ x6 . and (prim1 x6 (x3 x5)) (x4 = x0 x5 x6)).
The subproof is completed by applying unknownprop_d4dc73f3cbfe4c22363272ac418d035b8e77c49433b0870b96bee8fa9c46bfcf.