Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply unknownprop_c3fe42b21df0810041479a97b374de73f7754e07c8af1c88386a1e7dc0aad10f with
Sep x0 (λ x2 . x1 x2),
x0.
The subproof is completed by applying unknownprop_dde4f02836f1e21077854af0376b49f8617a754506141458ada04e8c79a76b89 with x0, x1.