Let x0 of type ι be given.

Assume H0: In x0 4.

Let x1 of type ι be given.

Assume H1: In x1 4.

Let x2 of type ι be given.

Assume H2: In x2 4.

Let x3 of type ι be given.

Assume H3: In x3 4.

Let x4 of type ι be given.

Assume H4: In x4 4.

Let x5 of type ι be given.

Assume H5: In x5 4.

Let x6 of type ι be given.

Assume H6: In x6 4.

Let x7 of type ι be given.

Assume H7: In x7 4.

Let x8 of type ι be given.

Assume H8: In x8 4.

Let x9 of type ι be given.

Assume H9: In x9 4.

Let x10 of type ι be given.

Assume H10: In x10 4.

Let x11 of type ι be given.

Assume H11: In x11 4.

Let x12 of type ι be given.

Assume H12: In x12 4.

Let x13 of type ι be given.

Assume H13: In x13 4.

Let x14 of type ι be given.

Assume H14: In x14 4.

Let x15 of type ι be given.

Assume H15: In x15 4.

Apply unknownprop_4952cbeaa3cfbe39042137e565a281ffc28405c7de4fe454358dcf1400b68a14 with 4, 44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15.

Let x16 of type ι be given.

Assume H16: In x16 4.

Let x17 of type ι be given.

Assume H17: In x17 4.

Apply unknownprop_0fadd198c09f8629cb4c152d61d82c413244246b3c85763ebe3d75aeff28b65a with x16, λ x18 . In (44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x18 x17) 4 leaving 5 subgoals.

The subproof is completed by applying H16.

Apply unknownprop_0fadd198c09f8629cb4c152d61d82c413244246b3c85763ebe3d75aeff28b65a with x17, λ x18 . In (44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 0 x18) 4 leaving 5 subgoals.

The subproof is completed by applying H17.

Apply unknownprop_69e449096c8c7f75b803b6f2b5996a6982049a86d4f472246439a923ae513a7c with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, λ x18 x19 . In x19 4.

The subproof is completed by applying H0.

Apply unknownprop_5d6a5fc8dec76e374b8c9f572ef6b40e9d95cf38c36afdc19c34e92f6ef5b3ca with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, λ x18 x19 . In x19 4.

The subproof is completed by applying H1.

Apply unknownprop_c0dfa089b59e6c022aac0a5812fe184e320375f837a8673d214f1add79026fa7 with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, λ x18 x19 . In x19 4.

The subproof is completed by applying H2.

Apply unknownprop_ae42978afe0561a6fe5e6c5b292421de928d8988b6ba3d972eac0b41a6d4fcb1 with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, λ x18 x19 . In x19 4.

The subproof is completed by applying H3.

Apply unknownprop_0fadd198c09f8629cb4c152d61d82c413244246b3c85763ebe3d75aeff28b65a with x17, λ x18 . In (44bc7.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 1 x18) 4 leaving 5 subgoals.

The subproof is completed by applying H17.

Apply unknownprop_786af4a8cc7ab24b71500b3f90e9fed430779ab18dc1ecd97f9d622d66e3769f with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, λ x18 x19 . In x19 4.

The subproof is completed by applying H4.

Apply unknownprop_b51a87b5b8d5fb1b58037ef724134f1b61cc1d3ba6729e58a1373e0efbaf0c61 with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, λ x18 x19 . In x19 4.

The subproof is completed by applying H5.

Apply unknownprop_543677efc8c023ad2c6b2666a49d8451c425d8c971324d9010f6bbc5e8694410 with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, λ x18 x19 . In x19 4.

The subproof is completed by applying H6.

Apply unknownprop_0772fcf1456bb34f4e88fcd5a35cdec280b1369383ba95078e3bfaad3e634252 with x0, x1, x2, x3, x4, x5, x6, ..., ..., ..., ..., ..., ..., ..., ..., ..., ....

...

■

Proofgold Proof