Let x0 of type ι be given.

Assume H0: In x0 3.

Let x1 of type ι be given.

Assume H1: In x1 3.

Let x2 of type ι be given.

Assume H2: In x2 3.

Let x3 of type ι be given.

Assume H3: In x3 3.

Let x4 of type ι be given.

Assume H4: In x4 3.

Let x5 of type ι be given.

Assume H5: In x5 3.

Let x6 of type ι be given.

Assume H6: In x6 3.

Let x7 of type ι be given.

Assume H7: In x7 3.

Let x8 of type ι be given.

Assume H8: In x8 3.

Apply unknownprop_4952cbeaa3cfbe39042137e565a281ffc28405c7de4fe454358dcf1400b68a14 with 3, 17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8.

Let x9 of type ι be given.

Assume H9: In x9 3.

Let x10 of type ι be given.

Assume H10: In x10 3.

Apply unknownprop_f20f08b38429d0914c6a2c13ffdd3fa446ab4342ea7a43d47915b2eca12847ee with x9, λ x11 . In (17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x11 x10) 3 leaving 4 subgoals.

The subproof is completed by applying H9.

Apply unknownprop_f20f08b38429d0914c6a2c13ffdd3fa446ab4342ea7a43d47915b2eca12847ee with x10, λ x11 . In (17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 0 x11) 3 leaving 4 subgoals.

The subproof is completed by applying H10.

Apply unknownprop_9939c8314afa4afce495b54e3f7722b610b588a4f22dde881d71d2681d672ab6 with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H0.

Apply unknownprop_9189e1e188ceb8273b08ea3bc9bc13e860cf3751901497cfb69acb9a5d855991 with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H1.

Apply unknownprop_11b6769e1852809e480368396b68112b14a0a4773d3ef45e8b4f6e9186d6f7f1 with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H2.

Apply unknownprop_f20f08b38429d0914c6a2c13ffdd3fa446ab4342ea7a43d47915b2eca12847ee with x10, λ x11 . In (17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 1 x11) 3 leaving 4 subgoals.

The subproof is completed by applying H10.

Apply unknownprop_9c8990e4433f05d7ad518ac341b5b45e2fc2242626b6960226ff3d2b9a1c7bf6 with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H3.

Apply unknownprop_bc85309a496692f6a1849136ee564cb8f1244fd2d094557e32eb16584df96f99 with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H4.

Apply unknownprop_3c071384429354d7a825435810a3f756fd7fdab458c90e623ebe4df76a5c2b25 with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H5.

Apply unknownprop_f20f08b38429d0914c6a2c13ffdd3fa446ab4342ea7a43d47915b2eca12847ee with x10, λ x11 . In (17ce0.. x0 x1 x2 x3 x4 x5 x6 x7 x8 2 x11) 3 leaving 4 subgoals.

The subproof is completed by applying H10.

Apply unknownprop_8f101177f1c41e2f0b64bdc7f8396b3d5b0a87c9af15b8fc3f7bac9ec78ad760 with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H6.

Apply unknownprop_f69a1b3d0586b140bb7e0c1f4a246c1554728ee9a4fefb99b908f872955cfd4d with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H7.

Apply unknownprop_b105c0d9fe0350df689bf180c5480ea21a0c8f3b78295648c79fbdf619c1e3fe with x0, x1, x2, x3, x4, x5, x6, x7, x8, λ x11 x12 . In x12 3.

The subproof is completed by applying H8.

■

Proofgold Proof