Apply unknownprop_5f29c1327d2c86d2bb80f30351058a3c8fd1b15045c54153ce3aff3f55e1b15c with
λ x0 x1 . TwoRamseyProp (ordsucc u4) (ordsucc u4) (ordsucc (ordsucc x0)).
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with
u4,
u4,
u31,
u31 leaving 4 subgoals.
The subproof is completed by applying unknownprop_723dd01f4e3b6ead0b114b6935717dcf3e97da79c873ecf977038ff266453fe1.
The subproof is completed by applying unknownprop_723dd01f4e3b6ead0b114b6935717dcf3e97da79c873ecf977038ff266453fe1.
Apply unknownprop_7bf6e58ac0649391f8a282bfdab147c48e1bbed6549cde1b2c604e23fd97b05e with
u4,
ordsucc u4,
ordsucc u31.
The subproof is completed by applying TwoRamseyProp_u4_u5_u32.
The subproof is completed by applying TwoRamseyProp_u4_u5_u32.