Claim L0: ∀ x0 : ι → ι → ι → ι → ι → ι → ι . Church6_p x0 ⟶ (λ x1 x2 . x2) = TwoRamseyGraph_4_6_Church6_squared_b (λ x1 x2 x3 x4 x5 x6 . x5) (λ x1 x2 x3 x4 x5 x6 . x5) (λ x1 x2 x3 x4 x5 x6 . x1) x0

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

Assume H0: Church6_p x0.

Apply H0 with λ x1 : ι → ι → ι → ι → ι → ι → ι . (λ x2 x3 . x3) = TwoRamseyGraph_4_6_Church6_squared_b (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x2) x1 leaving 6 subgoals.

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

Assume H1: x1 (λ x2 x3 . x3) (TwoRamseyGraph_4_6_Church6_squared_b (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x2) (λ x2 x3 x4 x5 x6 x7 . x2)).

The subproof is completed by applying H1.

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

Assume H1: x1 (λ x2 x3 . x3) (TwoRamseyGraph_4_6_Church6_squared_b (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x2) (λ x2 x3 x4 x5 x6 x7 . x3)).

The subproof is completed by applying H1.

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

Assume H1: x1 (λ x2 x3 . x3) (TwoRamseyGraph_4_6_Church6_squared_b (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x2) (λ x2 x3 x4 x5 x6 x7 . x4)).

The subproof is completed by applying H1.

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

Assume H1: x1 (λ x2 x3 . x3) (TwoRamseyGraph_4_6_Church6_squared_b (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x2) (λ x2 x3 x4 x5 x6 x7 . x5)).

The subproof is completed by applying H1.

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

Assume H1: x1 (λ x2 x3 . x3) (TwoRamseyGraph_4_6_Church6_squared_b (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x2) (λ x2 x3 x4 x5 x6 x7 . x6)).

The subproof is completed by applying H1.

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

Assume H1: x1 (λ x2 x3 . x3) (TwoRamseyGraph_4_6_Church6_squared_b (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x6) (λ x2 x3 x4 x5 x6 x7 . x2) (λ x2 x3 x4 x5 x6 x7 . x7)).

The subproof is completed by applying H1.

Let x0 of type ι be given.

Assume H1: x0 ∈ u6.

Apply unknownprop_d3b792af1adffec16ce4fc340f1433694e312f9a299dc66e7bdd660386d0095e with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . (u4 ∈ u6 ⟶ u4 ∈ u6 ⟶ 0 ∈ u6 ⟶ x0 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b x2 x2 (nth_6_tuple 0) (nth_6_tuple x0) = λ x3 x4 . x3) ⟶ False.

Apply unknownprop_5e063b347ef5ac56a92183cc00c589df53087ab1e0b6353a236a973dc2f46966 with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . (u4 ∈ u6 ⟶ u4 ∈ u6 ⟶ 0 ∈ u6 ⟶ x0 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) x2 (nth_6_tuple x0) = λ x3 x4 . x3) ⟶ False.

Assume H2: u4 ∈ u6 ⟶ u4 ∈ u6 ⟶ 0 ∈ u6 ⟶ x0 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (λ x1 x2 x3 x4 x5 x6 . x5) (λ x1 x2 x3 x4 x5 x6 . x5) (λ x1 x2 x3 x4 x5 x6 . x1) (nth_6_tuple x0) = λ x1 x2 . x1.

Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.

set y1 to be λ x1 x2 . x2

set y2 to be λ x2 x3 . x2

Claim L3: ∀ x3 : (ι → ι → ι) → ο . x3 y2 ⟶ x3 y1

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

Assume H3: x3 (λ x4 x5 . x4).

Apply L0 with nth_6_tuple y2, λ x4 : ι → ι → ι . x3 leaving 2 subgoals.

Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with y2.

The subproof is completed by applying H1.

Apply H2 with λ x4 : ι → ι → ι . x3 leaving 5 subgoals.

The subproof is completed by applying In_4_6.

The subproof is completed by applying In_0_6.

The subproof is completed by applying H1.

The subproof is completed by applying H3.

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

Apply L3 with λ x4 : ι → ι → ι . x3 x4 y2 ⟶ x3 y2 x4.

Assume H4: x3 y2 y2.

The subproof is completed by applying H4.

■

Proofgold Proof