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