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: x0 ∈ u6 ⟶ x1 ∈ u6 ⟶ x2 ∈ u6 ⟶ x3 ∈ u6 ⟶ TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) (nth_6_tuple x1) (nth_6_tuple x2) (nth_6_tuple x3) = λ x4 x5 . x4.

Assume H1: x2 ∈ u6.

Assume H2: x3 ∈ u6.

Assume H3: x0 ∈ u6.

Assume H4: x1 ∈ u6.

Apply unknownprop_4c4a30cb28bcd21744eec16e4ab4637f15035a845cbbb0ffbe052be5f3b1352d with x0, TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x2) (nth_6_tuple x3) (nth_6_tuple x0) (nth_6_tuple x1) = λ x4 x5 . x4 leaving 2 subgoals.

The subproof is completed by applying H3.

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

Assume H5: Church6_p x4.

Assume H6: x0 = Church6_to_u6 x4.

Apply unknownprop_4c4a30cb28bcd21744eec16e4ab4637f15035a845cbbb0ffbe052be5f3b1352d with x1, TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x2) (nth_6_tuple x3) (nth_6_tuple x0) (nth_6_tuple x1) = λ x5 x6 . x5 leaving 2 subgoals.

The subproof is completed by applying H4.

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

Assume H7: Church6_p x5.

Assume H8: x1 = Church6_to_u6 x5.

Apply H6 with λ x6 x7 . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x2) (nth_6_tuple x3) (nth_6_tuple x7) (nth_6_tuple x1) = λ x8 x9 . x8.

Apply H8 with λ x6 x7 . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x2) (nth_6_tuple x3) (nth_6_tuple (Church6_to_u6 x4)) (nth_6_tuple x7) = λ x8 x9 . x8.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x4, λ x6 x7 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x2) (nth_6_tuple x3) x7 (nth_6_tuple (Church6_to_u6 x5)) = λ x8 x9 . x8 leaving 2 subgoals.

The subproof is completed by applying H5.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x5, λ x6 x7 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x2) (nth_6_tuple x3) x4 x7 = λ x8 x9 . x8 leaving 2 subgoals.

The subproof is completed by applying H7.

Apply unknownprop_4c4a30cb28bcd21744eec16e4ab4637f15035a845cbbb0ffbe052be5f3b1352d with x2, TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x2) (nth_6_tuple x3) x4 x5 = λ x6 x7 . x6 leaving 2 subgoals.

The subproof is completed by applying H1.

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

Assume H9: Church6_p x6.

Assume H10: x2 = Church6_to_u6 x6.

Apply unknownprop_4c4a30cb28bcd21744eec16e4ab4637f15035a845cbbb0ffbe052be5f3b1352d with x3, TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x2) (nth_6_tuple x3) x4 x5 = λ x7 x8 . x7 leaving 2 subgoals.

The subproof is completed by applying H2.

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

Assume H11: Church6_p x7.

Assume H12: x3 = Church6_to_u6 x7.

Apply H10 with λ x8 x9 . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x9) (nth_6_tuple x3) x4 x5 = λ x10 x11 . x10.

Apply H12 with λ x8 x9 . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple (Church6_to_u6 x6)) (nth_6_tuple x9) x4 x5 = λ x10 x11 . x10.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x6, λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b x9 (nth_6_tuple (Church6_to_u6 x7)) x4 x5 = λ x10 x11 . x10 leaving 2 subgoals.

The subproof is completed by applying H9.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x7, λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b x6 x9 x4 x5 = λ x10 x11 . x10 leaving 2 subgoals.

The subproof is completed by applying H11.

Apply unknownprop_a6b94d39e112543346fd3d628055520b18b2a8c0ff7c088a719d9dfd3d3e8e01 with x4, x5, x6, x7 leaving 5 subgoals.

The subproof is completed by applying H5.

The subproof is completed by applying H7.

The subproof is completed by applying H9.

The subproof is completed by applying H11.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x4, λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b x8 x5 x6 x7 = λ x10 x11 . x10 leaving 2 subgoals.

The subproof is completed by applying H5.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x5, λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple (Church6_to_u6 x4)) x8 x6 x7 = λ x10 x11 . x10 leaving 2 subgoals.

The subproof is completed by applying H7.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x6, λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple (Church6_to_u6 x4)) (nth_6_tuple (Church6_to_u6 x5)) x8 x7 = λ x10 x11 . x10 leaving 2 subgoals.

The subproof is completed by applying H9.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x7, λ x8 x9 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple (Church6_to_u6 x4)) (nth_6_tuple ...) ... ... = ... leaving 2 subgoals.

...

■

Proofgold Proof