Apply unknownprop_e8139b4d35009943e50ba55c94172d08eb78b60f8fe4cab1d5f9f7c316f116d5 with
λ x0 x1 . TwoRamseyProp u3 u5 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
u2,
u4,
u9,
u5 leaving 4 subgoals.
The subproof is completed by applying nat_9.
The subproof is completed by applying nat_5.
Apply TwoRamseyProp_atleastp_atleastp with
u3,
u3,
u4,
u4,
u9 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_4_9.
The subproof is completed by applying atleastp_ref with
u3.
The subproof is completed by applying atleastp_ref with
u4.
The subproof is completed by applying unknownprop_678f269783f56623b590ce1d631178bc95b1ef296ba955ebeddcd0dc31626e86 with
u5.