Apply unknownprop_70a8ef6b90a3613f01ae6c665eced16b10e3c2de4bfc4352f3e312ab3c0845f2 with
λ x0 x1 . TwoRamseyProp 4 4 (ordsucc x0).
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
4,
4,
11 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_4_11.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 4.
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
3,
3,
11,
11 leaving 4 subgoals.
The subproof is completed by applying nat_11.
The subproof is completed by applying nat_11.
Apply unknownprop_9555e0d9fdb2de2946ade80c5601bbc2d7d10bbfbfdf3c2a29f338ee6ac35b14 with
3,
4,
11.
The subproof is completed by applying L0.
The subproof is completed by applying L0.