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

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

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

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

Assume H0: Church17_p x0.

Assume H1: Church17_p x1.

Assume H2: Church17_p x2.

Assume H3: Church17_p x3.

Assume H4: x0 = x1 ⟶ ∀ x4 : ο . x4.

Assume H5: x0 = x2 ⟶ ∀ x4 : ο . x4.

Assume H6: x0 = x3 ⟶ ∀ x4 : ο . x4.

Assume H7: x1 = x2 ⟶ ∀ x4 : ο . x4.

Assume H8: x1 = x3 ⟶ ∀ x4 : ο . x4.

Assume H9: x2 = x3 ⟶ ∀ x4 : ο . x4.

Assume H10: TwoRamseyGraph_4_4_Church17 x0 x1 = λ x4 x5 . x4.

Assume H11: TwoRamseyGraph_4_4_Church17 x0 x2 = λ x4 x5 . x4.

Assume H12: TwoRamseyGraph_4_4_Church17 x0 x3 = λ x4 x5 . x4.

Assume H13: TwoRamseyGraph_4_4_Church17 x1 x2 = λ x4 x5 . x4.

Assume H14: TwoRamseyGraph_4_4_Church17 x1 x3 = λ x4 x5 . x4.

Assume H15: TwoRamseyGraph_4_4_Church17 x2 x3 = λ x4 x5 . x4.

Apply unknownprop_0488073fe9c750b552eb460682a4287ceddcb40e6873677c84616c7fe9875c49 with x0, False leaving 2 subgoals.

The subproof is completed by applying H0.

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

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

Assume H16: ∀ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x6 ⟶ Church17_p (x4 x6).

Assume H17: ∀ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x6 ⟶ Church17_p (x5 x6).

Assume H18: ∀ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x4 (x5 x6) = x6.

Assume H19: ∀ x6 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 (x4 x6) = x6.

Assume H20: ∀ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . Church17_p x6 ⟶ Church17_p x7 ⟶ TwoRamseyGraph_4_4_Church17 x6 x7 = TwoRamseyGraph_4_4_Church17 (x4 x6) (x4 x7).

Assume H21: x4 x0 = λ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 . x6.

Apply unknownprop_5fd6939c226fd9da4e2a4a575d79a2e61666fad9c4051e73ef1851f344020124 with x4 x1, x4 x2, x4 x3 leaving 15 subgoals.

Apply H16 with x1.

The subproof is completed by applying H1.

Apply H16 with x2.

The subproof is completed by applying H2.

Apply H16 with x3.

The subproof is completed by applying H3.

Apply H21 with λ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x6 = x4 x1 ⟶ ∀ x8 : ο . x8.

Assume H22: x4 x0 = x4 x1.

Apply H4.

Apply H19 with x0, λ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x6 = x1.

Apply H19 with x1, λ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 (x4 x0) = x6.

set y6 to be x5 (x4 x0)

set y7 to be y6 (x5 x2)

Claim L23: ∀ x8 : (ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι) → ο . x8 y7 ⟶ x8 y6

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

Assume H23: x8 (y7 (y6 x3)).

set y9 to be λ x9 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x8

Apply H22 with λ x10 x11 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . y9 (y7 x10) (y7 x11).

The subproof is completed by applying H23.

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

Apply L23 with λ x9 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x8 x9 y7 ⟶ x8 y7 x9.

Assume H24: x8 y7 y7.

The subproof is completed by applying H24.

Apply H21 with λ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x6 = x4 x2 ⟶ ∀ x8 : ο . x8.

Assume H22: x4 x0 = x4 x2.

Apply H5.

Apply H19 with x0, λ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x6 = x2.

Apply H19 with x2, λ x6 x7 : ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι → ι . x5 (x4 x0) = x6.

set y6 to be ...

set y7 to be ...