Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_d1ab6c05d827ab2f0497648eeb2e74b0b0260f4e004a74cbc06a5c0a175e4a2a with
λ x2 x3 : ι → ι → ι → ι → ι → ι → ι . TwoRamseyGraph_4_6_Church6_squared_a (nth_6_tuple x0) (nth_6_tuple x1) x3 x3 = λ x4 x5 . x4.
Apply unknownprop_9250281955cc1f164124201c1f19b3e0fa9ad5273234f286ce461d841133e9cc with
nth_6_tuple x0,
nth_6_tuple x1 leaving 2 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.