Apply unknownprop_1accbadfa50080c0e26d369c4440fc6f34b7e7c33e9c1febe4b4ce000df77472.
Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
u4,
u4,
prim4 u4.
Apply TwoRamseyProp_atleastp_atleastp with
u4,
u4,
u5,
u4,
prim4 u4 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
u5,
u4 leaving 2 subgoals.
The subproof is completed by applying nat_5.
The subproof is completed by applying In_4_5.