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