Let x0 of type ι be given.

Assume H0: In x0 5.

Let x1 of type ι be given.

Assume H1: In x1 5.

Let x2 of type ι be given.

Assume H2: In x2 5.

Let x3 of type ι be given.

Assume H3: In x3 5.

Let x4 of type ι be given.

Assume H4: In x4 5.

Let x5 of type ι be given.

Assume H5: In x5 5.

Let x6 of type ι be given.

Assume H6: In x6 5.

Let x7 of type ι be given.

Assume H7: In x7 5.

Let x8 of type ι be given.

Assume H8: In x8 5.

Let x9 of type ι be given.

Assume H9: In x9 5.

Let x10 of type ι be given.

Assume H10: In x10 5.

Let x11 of type ι be given.

Assume H11: In x11 5.

Let x12 of type ι be given.

Assume H12: In x12 5.

Let x13 of type ι be given.

Assume H13: In x13 5.

Let x14 of type ι be given.

Assume H14: In x14 5.

Let x15 of type ι be given.

Assume H15: In x15 5.

Let x16 of type ι be given.

Assume H16: In x16 5.

Let x17 of type ι be given.

Assume H17: In x17 5.

Let x18 of type ι be given.

Assume H18: In x18 5.

Let x19 of type ι be given.

Assume H19: In x19 5.

Let x20 of type ι be given.

Assume H20: In x20 5.

Let x21 of type ι be given.

Assume H21: In x21 5.

Let x22 of type ι be given.

Assume H22: In x22 5.

Let x23 of type ι be given.

Assume H23: In x23 5.

Let x24 of type ι be given.

Assume H24: In x24 5.

Apply unknownprop_4952cbeaa3cfbe39042137e565a281ffc28405c7de4fe454358dcf1400b68a14 with 5, a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24.

Let x25 of type ι be given.

Assume H25: In x25 5.

Let x26 of type ι be given.

Assume H26: In x26 5.

Apply unknownprop_8ef96b8bfdfafc347c4af18ac841645c24347703f7d14928874fa7e0c39191e6 with x25, λ x27 . In (a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x27 x26) 5 leaving 6 subgoals.

The subproof is completed by applying H25.

Apply unknownprop_8ef96b8bfdfafc347c4af18ac841645c24347703f7d14928874fa7e0c39191e6 with x26, λ x27 . In (a80b3.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 0 x27) 5 leaving 6 subgoals.

The subproof is completed by applying H26.

Apply unknownprop_4962363bceed694252dd37a538631fb8511d2a5319cc3a3402fcf7a6420a9a03 with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, λ x27 x28 . In x28 5.

The subproof is completed by applying H0.

Apply unknownprop_198ab10e33d92ba95bc6a7c428aaab7427311751b5e4a4b93bd7101ee9d80f2e with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, λ x27 x28 . In x28 5.

The subproof is completed by applying H1.

Apply unknownprop_fbcf08b2a174b63c1dad365190335607c3c9cdd6915d4c9b02a6452e0b905b08 with x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, λ x27 x28 . In x28 5.

The subproof is completed by applying H2.

Apply unknownprop_b988f826e7116e177fcc6efefbc21efd6e236cddd3579b89c4a2cce21d2734bd with ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ..., ....

...

■

Proofgold Proof