Let x0 of type ι be given.
Let x1 of type (ι → ο) → ο be given.
Apply unknownprop_c44bc1e79e42a000a7340fdab78a639d4a425f294618f74dd3cf00309e4cf7e9 with
35104.. x0 x1,
x0,
x1.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H0.