Apply unknownprop_1871a7326a739d2e5a1c5a193f39d36fcf39c668bbe0796ca129e886d609d73d with
λ x0 x1 . TwoRamseyProp 4 5 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
3,
4,
23,
17 leaving 4 subgoals.
The subproof is completed by applying unknownprop_5a2415de7ce4ff7700953952ab57e066439372e1e8be58d2e9591f8d16f23b1d.
The subproof is completed by applying nat_17.
Apply TwoRamseyProp_atleastp_atleastp with
4,
4,
4,
4,
23 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_4_4_23.
The subproof is completed by applying atleastp_ref with 4.
The subproof is completed by applying atleastp_ref with 4.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
5,
5,
17 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_5_17.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 5.