Apply unknownprop_182c04046a079c94ddb7633eb3970f1d6314344011f16a11027ed1ec214739d8 with
λ x0 x1 : ι → ι → ι . ∀ x2 . ∀ x3 : ι → ι . ∀ x4 . prim1 x4 (0fc90.. x2 (λ x5 . x3 x5)) ⟶ x0 (f482f.. x4 4a7ef..) (f482f.. x4 (4ae4a.. 4a7ef..)) = x4.
The subproof is completed by applying unknownprop_06d1c1816b8dca9aa5139f4e37de734b4a0b4983a3b8804b34e381e7df94731b.