Apply unknownprop_9d9e6fc20609a6c2238d6d356ec8ab9dc460c51db2aad55ca748d2792a43e4dd with
λ x0 x1 . TwoRamseyProp 3 10 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
2,
9,
51,
10 leaving 4 subgoals.
The subproof is completed by applying unknownprop_0e4f7f5019dd72cad77d235851aaa5f40639940cef2c896847b5850af4193769.
The subproof is completed by applying nat_10.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
9,
9,
51 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_9_51.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 9.
The subproof is completed by applying unknownprop_678f269783f56623b590ce1d631178bc95b1ef296ba955ebeddcd0dc31626e86 with 10.