Apply unknownprop_88f2cfa93bbdf69d7deaded8c6678275a0bd7ea9bf3a688965672744594505a4 with
λ x0 x1 . TwoRamseyProp 4 8 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
3,
7,
99,
41 leaving 4 subgoals.
The subproof is completed by applying unknownprop_518f8766bcd89cc387e477ffe0d14cc0533a08b5c94d7cc56b6af58c2e4e9b47.
The subproof is completed by applying unknownprop_c2b569c4ea407208633a61660bb02890a0e91df6efa0f8aaeba9985b6978b990.
Apply TwoRamseyProp_atleastp_atleastp with
4,
4,
7,
7,
99 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_4_7_99.
The subproof is completed by applying atleastp_ref with 4.
The subproof is completed by applying atleastp_ref with 7.
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.