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 (3ffd5.. x1) x2 (3ffd5.. 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: 3ffd5.. x1 ∈ u6

Apply ordsuccI1 with ordsucc u4, 3ffd5.. x1.

Apply ordsuccI1 with u4, 3ffd5.. x1.

Apply unknownprop_cacb7c51f1a76b9ca3b0fd32a0e5e0cff86f3c58ae4158a5e5bfc653bbefb918 with x1.

The subproof is completed by applying H1.

Claim L9: 3ffd5.. x3 ∈ u6

Apply ordsuccI1 with ordsucc u4, 3ffd5.. x3.

Apply ordsuccI1 with u4, 3ffd5.. x3.

Apply unknownprop_cacb7c51f1a76b9ca3b0fd32a0e5e0cff86f3c58ae4158a5e5bfc653bbefb918 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_38257ef361f59f1bfc2dcda732163555f3f7a6ba9c09518c828159e997e214d4 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_8e2f777805a0d50c8eb492a93baff89a7be7ae44692bc8bd3afb9275a41b81f2 with x1, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) x5 (nth_6_tuple x2) (permargs_i_3_2_1_0_4_5 (nth_6_tuple x3)) = λ x6 x7 . x6 leaving 2 subgoals.

The subproof is completed by applying H1.

Apply unknownprop_8e2f777805a0d50c8eb492a93baff89a7be7ae44692bc8bd3afb9275a41b81f2 with x3, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_b (nth_6_tuple x0) (nth_6_tuple (3ffd5.. 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