Apply unknownprop_669df0da86db4f986bae532f93288cb46feb5b77310c7f6de7766507585de4c6 with
λ x0 x1 : ι → ι . ∀ x2 x3 x4 . prim1 x4 (aae7a.. x2 x3) ⟶ or (∃ x5 . and (prim1 x5 x2) (x4 = x0 x5)) (∃ x5 . and (prim1 x5 x3) (x4 = aae7a.. (4ae4a.. 4a7ef..) x5)).
Apply unknownprop_48f8d4859b6b78ba3bbfab79f28064a8eb2fee8b3008bbf7332b70f58b78e189 with
λ x0 x1 : ι → ι . ∀ x2 x3 x4 . prim1 x4 (aae7a.. x2 x3) ⟶ or (∃ x5 . and (prim1 x5 x2) (x4 = f6917.. x5)) (∃ x5 . and (prim1 x5 x3) (x4 = x0 x5)).
The subproof is completed by applying unknownprop_c7550417d862f27710857dc7f3a47fd61afe15d66581922367eb5c5641bfab12.