Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_8e2f777805a0d50c8eb492a93baff89a7be7ae44692bc8bd3afb9275a41b81f2 with
x1,
λ x4 x5 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) x4 (nth_6_tuple x2) (nth_6_tuple (3ffd5.. 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_a (nth_6_tuple x0) (permargs_i_3_2_1_0_4_5 (nth_6_tuple x1)) (nth_6_tuple x2) x4 = λ x6 x7 . x6 leaving 2 subgoals.
The subproof is completed by applying H3.
Apply unknownprop_6d71764a9a024a8f382431694d77ea6a197ff3b7947ee01f2f148455e062af95 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.
The subproof is completed by applying H4.