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 x3 x0.
The subproof is completed by applying unknownprop_98f3c840cba6bdce01722164c49b9631757b7c90bc7c46b34a7200f5fcc911e5 with x0, λ x3 . x1 x3, x2.