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