Apply unknownprop_4bc4e2cd6dce6ea21344ed15d01b94998744428f2a1e7eb15e38b5968b4c0663 with
λ x0 x1 . TwoRamseyProp 3 9 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
2,
8,
41,
9 leaving 4 subgoals.
Apply unknownprop_5a55ae6da060bd3592cd2518e6392e5786971bf34a92b383078bce38ef6a8408 with
ordsucc,
nat_p,
9 leaving 2 subgoals.
The subproof is completed by applying nat_ordsucc.
The subproof is completed by applying nat_9.
The subproof is completed by applying nat_9.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
8,
8,
41 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_8_41.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 8.
The subproof is completed by applying unknownprop_678f269783f56623b590ce1d631178bc95b1ef296ba955ebeddcd0dc31626e86 with 9.