Apply unknownprop_669df0da86db4f986bae532f93288cb46feb5b77310c7f6de7766507585de4c6 with
λ x0 x1 : ι → ι . ∀ x2 x3 x4 . prim1 x4 x2 ⟶ prim1 (x0 x4) (aae7a.. x2 x3).
The subproof is completed by applying unknownprop_8f6cc176a3f8bf2c7f1eddd738c1f22ef319b214b1baddc301c61e34c7bade15.