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