Apply unknownprop_6ec1a140d866846064cfd5c32674b693d943eda9dd3629a8fc81be59f6b279dd with
λ x0 x1 . TwoRamseyProp 5 6 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
4,
5,
83,
66 leaving 4 subgoals.
The subproof is completed by applying unknownprop_97adf820b20eeac6af845ba8e47a6fbaec6cf719d85196beb2a24f8a66ed4191.
The subproof is completed by applying unknownprop_6835fef0321aada2a10e29b89496f6c2c6a188b5ca1009dba36441f00472af29.
Apply TwoRamseyProp_atleastp_atleastp with
5,
5,
5,
5,
83 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_5_5_83.
The subproof is completed by applying atleastp_ref with 5.
The subproof is completed by applying atleastp_ref with 5.
Apply TwoRamseyProp_atleastp_atleastp with
4,
4,
6,
6,
66 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_4_6_66.
The subproof is completed by applying atleastp_ref with 4.
The subproof is completed by applying atleastp_ref with 6.