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