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)) ⟶ aae7a.. x3 (f482f.. x2 (4ae4a.. 4a7ef..)) = x2.
Apply unknownprop_fd8cfa9d525a4dec4072b8c89793bb3748a863e81655a11bd156798bb4989f99 with
x2,
λ x3 x4 . prim1 x2 (0fc90.. x0 (λ x5 . x1 x5)) ⟶ aae7a.. (e76d4.. x2) x3 = x2.
The subproof is completed by applying unknownprop_c8b63681804fba0e817d424dcd4474d1a0cb103b45a1fccf56209850a469b786 with x0, λ x3 . x1 x3, x2.