Apply unknownprop_df411260932bfc918d4ee62c114ac71f8ec98264037c12d71dfb9efc52a99615 with
λ x0 x1 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . 94591.. x1 (55574.. u19) = λ x2 x3 . x2.
Apply unknownprop_9ef01be1d276345c463186441a5675fe07097ab01b8002e94389de481ccaa0f8 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 . x20) 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 . x19) (λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x20)) (λ x1 x2 . x1).
The subproof is completed by applying H2.