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