Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ u4.

Let x2 of type ι be given.

Assume H2: x2 ∈ u6.

Let x3 of type ι be given.

Assume H3: x3 ∈ u4.

Assume H4: not (TwoRamseyGraph_4_6_35_b x0 x1 x2 x3).

Assume H5: TwoRamseyGraph_4_6_35_b x0 (247c9.. x1) x2 (247c9.. x3).

Claim L6: x1 ∈ u6

Apply ordsuccI1 with ordsucc u4, x1.

Apply ordsuccI1 with u4, x1.

The subproof is completed by applying H1.

Claim L7: x3 ∈ u6

Apply ordsuccI1 with ordsucc u4, x3.

Apply ordsuccI1 with u4, x3.

The subproof is completed by applying H3.

Claim L8: 247c9.. x1 ∈ u6

Apply ordsuccI1 with ordsucc u4, 247c9.. x1.

Apply ordsuccI1 with u4, 247c9.. x1.

Apply unknownprop_3cfa0e9ded071471f489f9c7aeb675465816cb9a2c40c37cd978c95d643f79eb with x1.

The subproof is completed by applying H1.

Claim L9: 247c9.. x3 ∈ u6

Apply ordsuccI1 with ordsucc u4, 247c9.. x3.

Apply ordsuccI1 with u4, 247c9.. x3.

Apply unknownprop_3cfa0e9ded071471f489f9c7aeb675465816cb9a2c40c37cd978c95d643f79eb with x3.

The subproof is completed by applying H3.

Apply H4.

Assume H10: x0 ∈ u6.

Assume H11: x1 ∈ u6.

Assume H12: x2 ∈ u6.

Assume H13: x3 ∈ u6.

Apply unknownprop_b3294a38b3b1f9d27668ff0beec69264c93c747df10829f156513becb3308a3f with nth_6_tuple x0, nth_6_tuple x1, nth_6_tuple x2, nth_6_tuple x3 leaving 5 subgoals.

Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x0.

The subproof is completed by applying H0.

Apply unknownprop_38a69925e68ff1a8dcf3a7f4e5069fa460ecf01c3c27215046eede1e2c2501a3 with x1.

The subproof is completed by applying H1.

Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x2.

The subproof is completed by applying H2.

Apply unknownprop_38a69925e68ff1a8dcf3a7f4e5069fa460ecf01c3c27215046eede1e2c2501a3 with x3.

The subproof is completed by applying H3.

Apply unknownprop_12a39fb3da1ba836f3fe134f631d49781d222ef9576bc8db0af83175e7b5b7fb with x1, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) x5 (nth_6_tuple x2) (permargs_i_2_3_0_1_4_5 (nth_6_tuple x3)) = λ x6 x7 . x6 leaving 2 subgoals.

The subproof is completed by applying H1.

Apply unknownprop_12a39fb3da1ba836f3fe134f631d49781d222ef9576bc8db0af83175e7b5b7fb with x3, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) (nth_6_tuple (247c9.. x1)) (nth_6_tuple x2) x5 = λ x6 x7 . x6 leaving 2 subgoals.

The subproof is completed by applying H3.

Apply H5 leaving 4 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying L8.

The subproof is completed by applying H2.

The subproof is completed by applying L9.

■

Proofgold Proof