Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
u4,
u4,
u18.
Apply unknownprop_344c784b1c3b94c370e58970c6c07f9652a98f817bb26a71614a2661ed1216a6 with
λ x0 x1 . TwoRamseyProp_atleastp (ordsucc u3) (ordsucc u3) (ordsucc (ordsucc x0)).
Apply TwoRamseyProp_atleastp_atleastp with
u3,
u3,
u4,
u4,
u9 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_4_9.
The subproof is completed by applying atleastp_ref with
u3.
The subproof is completed by applying atleastp_ref with
u4.
Apply unknownprop_2189d2fdc38fc21dedc845f1016855e7d4d32028f7f18ab941bdc60c8030f7be with
u3,
u3,
u8,
u8 leaving 4 subgoals.
The subproof is completed by applying nat_8.
The subproof is completed by applying nat_8.
Apply unknownprop_9555e0d9fdb2de2946ade80c5601bbc2d7d10bbfbfdf3c2a29f338ee6ac35b14 with
u3,
u4,
u9.
The subproof is completed by applying L0.
The subproof is completed by applying L0.