Let x0 of type ι be given.
Let x1 of type ι → ο be given.
Apply unknownprop_9a40b4678ae1931e61346f9ab9e405ec760f2f9d44b3be548b52a8b2ddb78559 with
x0,
Sep x0 x1.
The subproof is completed by applying unknownprop_ccf416ebcd13dfa730e29060b43bf042b51c2dc6688bd404c81b11af57f551d7 with x0, x1.