Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
ordsucc x0,
ordsucc x1,
ordsucc (ordsucc (add_nat x2 x3)).
Apply unknownprop_2189d2fdc38fc21dedc845f1016855e7d4d32028f7f18ab941bdc60c8030f7be with
x0,
x1,
x2,
x3 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply TwoRamseyProp_atleastp_atleastp with
ordsucc x0,
ordsucc x0,
x1,
x1,
ordsucc x2 leaving 3 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying atleastp_ref with
ordsucc x0.
The subproof is completed by applying atleastp_ref with x1.
Apply TwoRamseyProp_atleastp_atleastp with
x0,
x0,
ordsucc x1,
ordsucc x1,
ordsucc x3 leaving 3 subgoals.
The subproof is completed by applying H3.
The subproof is completed by applying atleastp_ref with x0.
The subproof is completed by applying atleastp_ref with
ordsucc x1.