Let x0 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

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

Let x2 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Let x3 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Let x4 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Let x5 of type ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → ((ι → ι) → ι → ι) → CN (ι → ι) be given.

Assume H0: ChurchNum_3ary_proj_p x0.

Assume H1: ChurchNum_3ary_proj_p x1.

Assume H2: ChurchNum_3ary_proj_p x2.

Assume H3: ChurchNum_8ary_proj_p x3.

Assume H4: ChurchNum_8ary_proj_p x4.

Assume H5: ChurchNum_8ary_proj_p x5.

Assume H6: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3 = λ x6 x7 . x6.

Apply unknownprop_2064d925adb7ad93ca392156fe7b0a7b799e0a1ed452f931aaf6d83e86b04609 with x0, x3, not (∀ x6 : ο . ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x8) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x14) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x1 x4 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x2 x5 = λ x6 x7 . x6) ⟶ (TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = λ x6 x7 . x6) ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 ⟶ ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 ⟶ ChurchNums_3x8_neq x0 x3 x1 x4 ⟶ ChurchNums_3x8_neq x0 x3 x2 x5 ⟶ ChurchNums_3x8_neq x1 x4 x2 x5 ⟶ False leaving 14 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H3.

The subproof is completed by applying H6.

Assume H7: x0 = λ x6 x7 x8 : (ι → ι) → ι → ι . x6.

Assume H8: x3 = λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6.

Assume H9: not (∀ x6 : ο . ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x7) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x8) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x8) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x14) ⟶ x6) ⟶ ((x0 = λ x7 x8 x9 : (ι → ι) → ι → ι . x9) ⟶ (x3 = λ x7 x8 x9 x10 x11 x12 x13 x14 : (ι → ι) → ι → ι . x11) ⟶ x6) ⟶ x6).

Assume H10: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x1 x4 = λ x6 x7 . x6.

Assume H11: TwoRamseyGraph_4_5_24_ChurchNums_3x8 (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x2 x5 = λ x6 x7 . x6.

Assume H12: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x1 x4 = λ x6 x7 . x6.

Assume H13: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x0 x3 x2 x5 = λ x6 x7 . x6.

Assume H14: TwoRamseyGraph_4_5_24_ChurchNums_3x8 x1 x4 x2 x5 = λ x6 x7 . x6.

Assume H15: ChurchNums_3x8_neq (λ x6 x7 x8 : (ι → ι) → ι → ι . x6) (λ x6 x7 x8 x9 x10 x11 x12 x13 : (ι → ι) → ι → ι . x6) x0 x3.

Apply H15 with ... ⟶ ... ⟶ ... ⟶ ChurchNums_3x8_neq x0 x3 x2 x5 ⟶ ChurchNums_3x8_neq x1 x4 x2 x5 ⟶ False.

...

■

Proofgold Proof