Apply unknownprop_d32c2e377314b1972e17c149653f6099c7ac9647b19ffa42c03b41634506f348 with
λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. x1 (55574.. u20) = λ x2 x3 . x2.
Apply unknownprop_cef52413820f1260ec1695f1f292d8e88151d0531a1ef8c4f2ae82c3cd4779d4 with
λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x19) x1 = λ x2 x3 . x2.
Let x0 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H2:
x0 (94591.. (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x18) (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x21)) (λ x1 x2 . x1).
The subproof is completed by applying H2.