Let x0 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.

Let x1 of type ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι be given.

Assume H0: Church13_p x0.

Assume H1: Church13_p x1.

Apply H0 with λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_5_Church13 x2 x1 = TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x2) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x1) leaving 13 subgoals.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) x2 = TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x2) leaving 13 subgoals.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x5)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x5))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x7)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x7))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x8)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x8))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x9)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x9))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x10)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x10))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x11)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x11))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x12)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x12))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x13)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x13))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x14)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x14))).

The subproof is completed by applying H2.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x15)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x15))).

The subproof is completed by applying H2.

Apply H1 with λ x2 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4) x2 = TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4)) (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 x2) leaving 13 subgoals.

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

Assume H2: x2 (TwoRamseyGraph_3_5_Church13 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4) (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x3)) (TwoRamseyGraph_3_5_Church13 (Church13_perm_8_9_10_11_12_0_1_2_3_4_5_6_7 (λ x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x4)) ...).

...

■

Proofgold Proof