Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_e65d4a6131bd0f3fcd91fa1f20b9cfd36b0cf97f8c821750cc7f8f971a40e6bb with
x0,
x1,
x1.
The subproof is completed by applying unknownprop_6720ce2f41db96364ddfead9c4fd7465c9ef398fd81171f82dc50bd2f1d3c744 with
x0,
λ x2 . In x2 x1.