Let x0 of type ι be given.

Assume H0: x0 ∈ u6.

Let x1 of type ι be given.

Assume H1: x1 ∈ u6.

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

The subproof is completed by applying H0.

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

Assume H2: Church6_p x2.

Assume H3: x0 = Church6_to_u6 x2.

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

The subproof is completed by applying H1.

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

Assume H4: Church6_p x3.

Assume H5: x1 = Church6_to_u6 x3.

Apply H3 with λ x4 x5 . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x5) (nth_6_tuple x1) (nth_6_tuple x5) (nth_6_tuple x1) = λ x6 x7 . x6.

Apply H5 with λ x4 x5 . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple (Church6_to_u6 x2)) (nth_6_tuple x5) (nth_6_tuple (Church6_to_u6 x2)) (nth_6_tuple x5) = λ x6 x7 . x6.

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

The subproof is completed by applying H2.

Apply unknownprop_1df6cb25245842ac80f846f984ad1ab224979cc48aebddb9e27917721a4b0bdb with x3, λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a x2 x5 x2 x5 = λ x6 x7 . x6 leaving 2 subgoals.

The subproof is completed by applying H4.

Apply unknownprop_0aca25f61c76eaca3e268d1d74d81b05f2393e00014195cda2f42fba2f21a963 with x2, x3 leaving 2 subgoals.

The subproof is completed by applying H2.

The subproof is completed by applying H4.

■

Proofgold Proof