Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_4c7c6a01193a68b8e5840b3e04313713b98b7f4e59d0d80bcd9a29ba93e073e2 with
x0,
x1,
λ x2 . x2.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H0 with λ x3 x4 . x2 x4 x3.