Let x0 of type ι be given.
Let x1 of type ι → ι → ι be given.
Let x2 of type ι → ο be given.
Apply unknownprop_bd647b72bbc4a85252654132c2274ee3e808ed27529cc4ab5374fb42261ed5fd with
33a0d.. x0 x1 x2,
x0,
x1,
x2.
Let x3 of type ι → ι → ο be given.
The subproof is completed by applying H0.