Apply unknownprop_2d32a432b91f373691a1836f6bf2aa293c213f207ed6ef9525f7d1d01aa1abda with
λ x0 x1 . TwoRamseyProp 4 6 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
3,
5,
41,
24 leaving 4 subgoals.
The subproof is completed by applying unknownprop_c2b569c4ea407208633a61660bb02890a0e91df6efa0f8aaeba9985b6978b990.
The subproof is completed by applying unknownprop_a7f3578ada9cacf1cb3296f5290d2c691e8a6f96bb11bbe9193ef025e25fc69a.
Apply TwoRamseyProp_atleastp_atleastp with
4,
4,
5,
5,
41 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_4_5_41.
The subproof is completed by applying atleastp_ref with 4.
The subproof is completed by applying atleastp_ref with 5.
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.