Let x0 of type ι be given.
Let x1 of type ι → ι be given.
Let x2 of type ι be given.
Apply unknownprop_da2bd49e935d53cfac7d2dade92fed0a4715f02a565c10e2712c01b04174bdd7 with
x2,
λ x3 x4 . prim1 x2 (0fc90.. x0 (λ x5 . x1 x5)) ⟶ prim1 (f482f.. x2 (4ae4a.. 4a7ef..)) (x1 x3).
Apply unknownprop_fd8cfa9d525a4dec4072b8c89793bb3748a863e81655a11bd156798bb4989f99 with
x2,
λ x3 x4 . prim1 x2 (0fc90.. x0 (λ x5 . x1 x5)) ⟶ prim1 x3 (x1 (e76d4.. x2)).
The subproof is completed by applying unknownprop_39778cd4b79940b57d8e2a75e110efc525ea390ceb2294eb222b7e4525c53c50 with x0, λ x3 . x1 x3, x2.