Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Apply unknownprop_708728ae3ee0c77117f893e7562991e35de4f455e0b3d6b9d1ab42e0388e7561 with
987b2.. x0 x1,
x0,
x1.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H0.