Apply unknownprop_3259cb7d3b3b3adafac7093356c6be4d14cc142aba0c3345c772dc583fe3fafc with
λ x0 x1 . TwoRamseyProp 3 6 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
2,
5,
17,
6 leaving 4 subgoals.
The subproof is completed by applying nat_17.
The subproof is completed by applying nat_6.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
5,
5,
17 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_5_17.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 5.
The subproof is completed by applying unknownprop_678f269783f56623b590ce1d631178bc95b1ef296ba955ebeddcd0dc31626e86 with 6.