Let x0 of type ι → ι → ο be given.
Let x1 of type ι → ι → ο be given.
Apply unknownprop_5dbf3e44f293aa5024c406dda8d77437ab46c5dd1421655e71b5703836ad19b7 with
x0,
x1,
32d20...
The subproof is completed by applying unknownprop_2c6d593894296c84c8495112a34fbf463ff3a0139d6c76449529901af9854967 with
x0,
x1,
5c39b...