Let x0 of type ι be given.

Assume H0: x0 ∈ u22.

Let x1 of type (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο be given.

Assume H1: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x2).

Assume H2: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x3).

Assume H3: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x4).

Assume H4: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x5).

Assume H5: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x6).

Assume H6: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x7).

Assume H7: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x8).

Assume H8: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x9).

Assume H9: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x10).

Assume H10: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x11).

Assume H11: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x12).

Assume H12: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x13).

Assume H13: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x14).

Assume H14: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x15).

Assume H15: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x16).

Assume H16: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x17).

Assume H17: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x18).

Assume H18: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x19).

Assume H19: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x20).

Assume H20: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x21).

Assume H21: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x22).

Assume H22: x1 (λ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 . x23).

Apply unknownprop_d063ce03105999ee16bbafa5f65220ff2535b43f3c3d0afd7d320f4f3006227c with x0, λ x2 . x1 (55574.. x2) leaving 23 subgoals.

The subproof is completed by applying H0.

Apply unknownprop_185e94e662a577fb5e2b92ce52649a1318311ab8e572939affacc9b7c5235200 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H1.

Apply unknownprop_6479a43174f47c77b90f2d570c9fecae99b692135893ea46f64f47a06da93bf8 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H2.

Apply unknownprop_7d6f755c8dc7037da5498a72b88a0cb818b42f84cba832342d390734f147b368 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H3.

Apply unknownprop_8e3d5e1e685ab84aae0f743c0b732bb799e24a94acca6d58b1f9c3647fe54de9 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H4.

Apply unknownprop_a1719a78bccce8b617c9ce09b8876e026b18c9e6801e3656811b5bf0d98e937e with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H5.

Apply unknownprop_3f3ef00c9e6004b683c5120ebd9cf81db16a7a3cd1c3294ce2b72258997c9e16 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H6.

Apply unknownprop_a968794b819a10962bb214e36aefd50bb7d3d7924a887bcfb206107787ce7029 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H7.

Apply unknownprop_12e7d4db4dc26ec8e0da3893682b1e7a082b06b5ddf76e8c938f7c99fba3ef27 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H8.

Apply unknownprop_802fc62c12be2c3f0be67b0e735217cafea534b51b986b164be966194e9f1ded with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H9.

Apply unknownprop_33c0b4024debf64e7c4f093be21083181db5220b193b69b592427679bce6fcb9 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H10.

Apply unknownprop_8e321c9891c866336dee40a53046c3156fb71320e2aecc12d0d23848d25a78f7 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H11.

Apply unknownprop_6a1304f877c3c02d89f43dc17dde60ba61f377b2952b008d1ad7ddcc6dc6f46d with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H12.

Apply unknownprop_750bbfd209cbbc2638525ff49836b8d57a9d46b5b0085915178b80f8528ec332 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H13.

Apply unknownprop_18eebfd25a7331a0b2ce344c74195903de0eaf16c158101d3e233a5c6da08efd with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H14.

Apply unknownprop_f953daabedd60bf9f93079f217c6737ebd2588040f321df41596b9904e806c99 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H15.

Apply unknownprop_a37ba53c5df23420c1ecc0f74797b2b4fd31257965cf312a41a8ad8d05ee9d50 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H16.

Apply unknownprop_8bc547942d421befdbf9d90bb1a04d6f3b4023e0fb5e66858447e172d6368c6e with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H17.

Apply unknownprop_d32c2e377314b1972e17c149653f6099c7ac9647b19ffa42c03b41634506f348 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H18.

Apply unknownprop_df411260932bfc918d4ee62c114ac71f8ec98264037c12d71dfb9efc52a99615 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H19.

Apply unknownprop_9ef01be1d276345c463186441a5675fe07097ab01b8002e94389de481ccaa0f8 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H20.

Apply unknownprop_cef52413820f1260ec1695f1f292d8e88151d0531a1ef8c4f2ae82c3cd4779d4 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H21.

Apply unknownprop_58d7e58252715f4e93831a23afca08961a0fe3cb854c045874e6ecb879335e52 with λ x2 x3 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x1 x3.

The subproof is completed by applying H22.

■

Proofgold Proof