Let x0 of type ι → ο be given.
Let x1 of type (ι → ο) → ι → ο be given.
Apply unknownprop_48bdd6a657f347e61951e7c156219665659681230736ec34551e878152deeb27 with
x0,
λ x2 . x2,
λ x2 : ι → ο . λ x3 . x1 x2 x3.
Let x2 of type ι be given.
Apply unknownprop_97cd06c26cc6b1274a544bade30e933631c1992e032574c4fe030a3cab228183 with
de327.. x0 x2,
x2.
The subproof is completed by applying unknownprop_8d6cc1e368ee396f68b51d3338711391f5208d276bde615adf4b4d34a28891f9 with x0, x2.