Apply unknownprop_182c04046a079c94ddb7633eb3970f1d6314344011f16a11027ed1ec214739d8 with
λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 . prim1 x4 x2 ⟶ prim1 (x0 4a7ef.. x4) (x0 x2 x3).
The subproof is completed by applying unknownprop_06cf747e8d9f0e35f7afc6431ac124a9c5ccd5d57328e22bb582431e9562acba.