Apply unknownprop_0ab0f3bd8351c27d763063f15ec4b3e9dd38d8c64505f2de3a82cb8384f460b9 with
λ x0 x1 . TwoRamseyProp 3 7 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
2,
6,
24,
7 leaving 4 subgoals.
The subproof is completed by applying unknownprop_a7f3578ada9cacf1cb3296f5290d2c691e8a6f96bb11bbe9193ef025e25fc69a.
The subproof is completed by applying nat_7.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
6,
6,
24 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_6_24.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 6.
The subproof is completed by applying unknownprop_678f269783f56623b590ce1d631178bc95b1ef296ba955ebeddcd0dc31626e86 with 7.