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

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

Assume H0: Church6_p x0.

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

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

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

The subproof is completed by applying H1.

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

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

The subproof is completed by applying H1.

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

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

The subproof is completed by applying H1.

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

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

The subproof is completed by applying H1.

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

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

The subproof is completed by applying H1.

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

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

The subproof is completed by applying H1.

Let x0 of type ι be given.

Assume H1: x0 ∈ u6.

Apply unknownprop_d3b792af1adffec16ce4fc340f1433694e312f9a299dc66e7bdd660386d0095e with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a x2 x2 (nth_6_tuple u5) (nth_6_tuple x0) = λ x3 x4 . x3.

Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with λ x1 x2 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (λ x3 x4 x5 x6 x7 x8 . x7) (λ x3 x4 x5 x6 x7 x8 . x7) x2 (nth_6_tuple x0) = λ x3 x4 . x3.

Apply L0 with nth_6_tuple x0.

Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x0.

The subproof is completed by applying H1.

■

Proofgold Proof