Apply unknownprop_d32c2e377314b1972e17c149653f6099c7ac9647b19ffa42c03b41634506f348 with
λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. x1 (55574.. u18) = λ x2 x3 . x2.
Apply unknownprop_df411260932bfc918d4ee62c114ac71f8ec98264037c12d71dfb9efc52a99615 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 . x19)) (λ x1 x2 . x1).
The subproof is completed by applying H2.