Apply unknownprop_61a679b0722df88389d2922bd7db003bc3daa7472bfca90e161a143841c76892 with
λ x0 x1 . TwoRamseyProp 4 7 (ordsucc x0).
Apply unknownprop_217e5145b65197888461a6aa126b20121c0d56dc8d69d44ac11b973377d98f71 with
3,
6,
66,
32 leaving 4 subgoals.
The subproof is completed by applying unknownprop_6835fef0321aada2a10e29b89496f6c2c6a188b5ca1009dba36441f00472af29.
The subproof is completed by applying unknownprop_e20297641bb65d9e51ebac2e053948365a3f53b65d223d41920ce90b2e26b533.
Apply TwoRamseyProp_atleastp_atleastp with
4,
4,
6,
6,
66 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_4_6_66.
The subproof is completed by applying atleastp_ref with 4.
The subproof is completed by applying atleastp_ref with 6.
Apply TwoRamseyProp_atleastp_atleastp with
3,
3,
7,
7,
32 leaving 3 subgoals.
The subproof is completed by applying TwoRamseyProp_3_7_32.
The subproof is completed by applying atleastp_ref with 3.
The subproof is completed by applying atleastp_ref with 7.