Let x0 of type ι → ι → ι be given.
Let x1 of type ι → ι → ι be given.
Apply H0 with
λ x2 x3 : ι → ι → ι . 6fb7f.. (cc64c.. x3 x1).
Apply unknownprop_fe36caae5784dcaccf90e3c33c4c3db05a48fc46bf7e1321a13b032e9121e798 with
λ x2 x3 : ι → ι → ι . 6fb7f.. (λ x4 x5 . x3 x4 (x1 x4 x5)).
The subproof is completed by applying H1.