Apply unknownprop_182c04046a079c94ddb7633eb3970f1d6314344011f16a11027ed1ec214739d8 with
λ x0 x1 : ι → ι → ι . ∀ x2 x3 x4 . prim1 x4 x3 ⟶ prim1 (x0 (4ae4a.. 4a7ef..) x4) (x0 x2 x3).
The subproof is completed by applying unknownprop_b4a3840982f4171d50a8011f1d1ddb72ad2a6c5880e9b141f24bf23602367bb7.