Apply functional extensionality with
09364..,
aae7a.. (4ae4a.. 4a7ef..).
Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying unknownprop_497ceb2eb28aaf14c46cc38f218092e3e652567d5b5313af58a8c57d6bddfd1b with x0, λ x2 x3 . x1 x3 x2.