Apply unknownprop_bc7bb32ef10cfe64d441ac6f7b6d6067caca25b88a2ca005e873f54e22a2dcde with
λ x0 x1 . TwoRamseyProp 3 8 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
2,
7,
32,
8 leaving 4 subgoals.
The subproof is completed by applying unknownprop_e20297641bb65d9e51ebac2e053948365a3f53b65d223d41920ce90b2e26b533.
The subproof is completed by applying nat_8.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
7,
7,
32 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_7_32.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 7.
The subproof is completed by applying unknownprop_678f269783f56623b590ce1d631178bc95b1ef296ba955ebeddcd0dc31626e86 with 8.