Let x0 of type ο be given.
Let x1 of type ι → ι be given.
Let x2 of type ι → ι be given.
Apply functional extensionality with
711f6.. x0 x1 x2,
x2.
Let x3 of type ι be given.
Apply unknownprop_5a150bd86f4285de5d98c60b17d4452a655b4d88de0a02247259cdad6e6d992c with
x0,
x1 x3,
x2 x3.
The subproof is completed by applying H0.