Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ u6.

Let x2 of type ι be given.

Assume H2: x2 ∈ u6.

Let x3 of type ι be given.

Assume H3: x3 ∈ u6.

Assume H4: TwoRamseyGraph_4_6_35_a x0 x1 x2 x3.

Apply unknownprop_3db87ec95ff0905d0301ba501c5a7b083bd23f41cda3e6500489fcc87ee60278 with x0, x1, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) x4 (nth_6_tuple x2) (nth_6_tuple (u6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 x2 x3)) = λ x6 x7 . x6 leaving 3 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

Apply unknownprop_3db87ec95ff0905d0301ba501c5a7b083bd23f41cda3e6500489fcc87ee60278 with x2, x3, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) (Church6_squared_permutation__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5__3_2_1_0_4_5 (nth_6_tuple x0) (nth_6_tuple x1)) (nth_6_tuple x2) x4 = λ x6 x7 . x6 leaving 3 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H3.

Apply unknownprop_188441ec85bf86a2c57fc04f16adf19032ec3c6e4c4ad9f5da48d85aed64a49a 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_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x1.

The subproof is completed by applying H1.

Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x2.

The subproof is completed by applying H2.

Apply unknownprop_90460311f4fb47844a8dd0d64a1306416f6a25ac4d465fc1811061f42791aace with x3.

The subproof is completed by applying H3.

The subproof is completed by applying H4.

■

Proofgold Proof