Apply not_TwoRamseyProp_4_6_Power_5.
Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
4,
6,
prim4 5.
Apply TwoRamseyProp_atleastp_atleastp with
u4,
u4,
u7,
u6,
prim4 u5 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying atleastp_ref with
u4.
Apply nat_In_atleastp with
u7,
u6 leaving 2 subgoals.
The subproof is completed by applying nat_7.
The subproof is completed by applying In_6_7.