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

Apply ordsuccI1 with ordsucc u4, 9defa.. x1.

Apply ordsuccI1 with u4, 9defa.. x1.

Apply unknownprop_ae688c06941cbaa572ade457c56bbb42cc75c9441f6000649a99d70e55ce0805 with x1.

The subproof is completed by applying H1.

Claim L9: 9defa.. x3 ∈ u6

Apply ordsuccI1 with ordsucc u4, 9defa.. x3.

Apply ordsuccI1 with u4, 9defa.. x3.

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

The subproof is completed by applying H1.

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