Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_faec30ccee17d5393df69f9f5bea99ea0c13abcbefd6cdd0db4986d76425691f with
x0,
x1,
λ x2 x3 . aae7a.. x3 (f482f.. (aae7a.. x0 x1) (4ae4a.. 4a7ef..)) = aae7a.. x0 x1.
Apply unknownprop_9dd94f511a765d0ea093bc5fe699c952238c27065924c5579c270577f2c40c04 with
x0,
x1,
λ x2 x3 . aae7a.. x0 x3 = aae7a.. x0 x1.
Let x2 of type ι → ι → ο be given.
The subproof is completed by applying H0.