Let x0 of type ι be given.
Let x1 of type ι be given.
Apply xm with
x0 ∈ u17,
0aea9.. x0 x1 ⟶ 0aea9.. x1 x0 leaving 2 subgoals.
Apply xm with
x1 ∈ u17,
0aea9.. x0 x1 ⟶ 0aea9.. x1 x0 leaving 2 subgoals.
Apply unknownprop_331d7f66eeb37dc381bf2e3606d3b3c601f9b8768b689e8985564581b76a5fdc with
x1,
x0 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply unknownprop_5cece90b225888ed5e86060411031b7dea9c395004ca9e7ebb9069250f2769f8 with
x0,
x1.
Apply unknownprop_e16ab3d50baafeaf90a0ee1065332204d3827bebf1dd68c1acb8dccd52cf984e with
x0,
x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_14e19ebc7e16f882d3be4482dbe497cecb7597969c9cae0a9f87fe87a0ee217a with
x0,
λ x2 . (94591.. (55574.. x2) (55574.. x1) = λ x3 x4 . x3) ⟶ 94591.. (55574.. x1) (55574.. x2) = λ x3 x4 . x3 leaving 19 subgoals.
The subproof is completed by applying H0.
Apply unknownprop_185e94e662a577fb5e2b92ce52649a1318311ab8e572939affacc9b7c5235200 with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (94591.. x3 (55574.. x1) = λ x4 x5 . x4) ⟶ 94591.. (55574.. x1) x3 = λ x4 x5 . x4.
Apply unknownprop_385697d8441c5f778e16c97ac3fd3d842ad68223c4d1882ce705cb1375e178b5 with
x1,
λ x2 . (94591.. (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x3) (55574.. x2) = λ x3 x4 . x3) ⟶ 94591.. (55574.. x2) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x3) = λ x3 x4 . x3 leaving 6 subgoals.
The subproof is completed by applying L5.
Apply unknownprop_d32c2e377314b1972e17c149653f6099c7ac9647b19ffa42c03b41634506f348 with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (94591.. (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) x3 = λ x4 x5 . x4) ⟶ 94591.. x3 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) = λ x4 x5 . x4.
Assume H6:
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x19) = λ x2 x3 . x2.
Let x2 of type (ι → ι → ι) → (ι → ι → ι) → ο be given.
Assume H7:
x2 (94591.. (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x20) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 . x3)) (λ x3 x4 . x3).
The subproof is completed by applying H7.
Apply unknownprop_df411260932bfc918d4ee62c114ac71f8ec98264037c12d71dfb9efc52a99615 with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (94591.. (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) x3 = λ x4 x5 . x4) ⟶ 94591.. x3 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) = λ x4 x5 . x4.
Assume H6:
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x20) = λ x2 x3 . x2.
Apply FalseE with
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x20) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) = λ x2 x3 . x2.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
The subproof is completed by applying H6.
Apply unknownprop_9ef01be1d276345c463186441a5675fe07097ab01b8002e94389de481ccaa0f8 with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (94591.. (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) x3 = λ x4 x5 . x4) ⟶ 94591.. x3 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) = λ x4 x5 . x4.
Assume H6:
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x21) = λ x2 x3 . x2.
Apply FalseE with
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x21) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) = λ x2 x3 . x2.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
The subproof is completed by applying H6.
Apply unknownprop_cef52413820f1260ec1695f1f292d8e88151d0531a1ef8c4f2ae82c3cd4779d4 with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (94591.. (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) x3 = λ x4 x5 . x4) ⟶ 94591.. x3 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) = λ x4 x5 . x4.
Assume H6:
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x22) = λ x2 x3 . x2.
Apply FalseE with
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x22) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) = λ x2 x3 . x2.
Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.
The subproof is completed by applying H6.
Apply unknownprop_58d7e58252715f4e93831a23afca08961a0fe3cb854c045874e6ecb879335e52 with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . (94591.. (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) x3 = λ x4 x5 . x4) ⟶ 94591.. x3 (λ x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 . x4) = λ x4 x5 . x4.
Assume H6:
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x23) = λ x2 x3 . x2.
Apply FalseE with
94591.. (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x23) (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2) = λ x2 x3 . ....