Apply unknownprop_eb408a95f5e91aab2702f4647edd22de7fa23c52e959ad43a388df4cef776ad7 with
λ x0 x1 . TwoRamseyProp 5 5 (ordsucc x0).
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 unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
4,
4,
41,
41 leaving 4 subgoals.
The subproof is completed by applying unknownprop_c2b569c4ea407208633a61660bb02890a0e91df6efa0f8aaeba9985b6978b990.
The subproof is completed by applying unknownprop_c2b569c4ea407208633a61660bb02890a0e91df6efa0f8aaeba9985b6978b990.
Apply unknownprop_9555e0d9fdb2de2946ade80c5601bbc2d7d10bbfbfdf3c2a29f338ee6ac35b14 with
4,
5,
41.
The subproof is completed by applying L0.
The subproof is completed by applying L0.