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