Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ u6.

Apply unknownprop_4c4a30cb28bcd21744eec16e4ab4637f15035a845cbbb0ffbe052be5f3b1352d with x0, not (x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x0) (nth_6_tuple x1) = λ x2 x3 . x2) leaving 2 subgoals.

The subproof is completed by applying H0.

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

Assume H2: Church6_p x2.

Assume H3: x0 = Church6_to_u6 x2.

Apply unknownprop_4c4a30cb28bcd21744eec16e4ab4637f15035a845cbbb0ffbe052be5f3b1352d with x1, not (x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x0) (nth_6_tuple x1) = λ x3 x4 . x3) leaving 2 subgoals.

The subproof is completed by applying H1.

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

Assume H4: Church6_p x3.

Assume H5: x1 = Church6_to_u6 x3.

Apply H3 with λ x4 x5 . not (x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x5) (nth_6_tuple x1) (nth_6_tuple x5) (nth_6_tuple x1) = λ x6 x7 . x6).

Apply H5 with λ x4 x5 . not (x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple (Church6_to_u6 x2)) (nth_6_tuple x5) (nth_6_tuple (Church6_to_u6 x2)) (nth_6_tuple x5) = λ x6 x7 . x6).

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x2, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . not (x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b x5 (nth_6_tuple (Church6_to_u6 x3)) x5 (nth_6_tuple (Church6_to_u6 x3)) = λ x6 x7 . x6) leaving 2 subgoals.

The subproof is completed by applying H2.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x3, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . not (x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b x2 x5 x2 x5 = λ x6 x7 . x6) leaving 2 subgoals.

The subproof is completed by applying H4.

Assume H6: x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b x2 x3 x2 x3 = λ x4 x5 . x4.

Claim L7: TwoRamseyGraph_4_6_Church6_squared_b x2 x3 x2 x3 = λ x4 x5 . x4

Apply H6 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply unknownprop_1019f796b5519c5beeeef55b1daae2de48848a97e75d217687db0a2449fd5208.

Apply L7 with λ x4 x5 : ι → ι → ι . (λ x6 x7 . x7) = x4.

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

Apply unknownprop_7a4d4f9c44385bd11ea934f1cc90d5fd8ad2ebc9d1a7bdb16e45d41bd3fe96f0 with x2, x3, λ x5 x6 : ι → ι → ι . x4 x6 x5 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H4.

■

Proofgold Proof