Apply unknownprop_6cbf2ce5b238902a91be96bb2397d1da08ec04d3fb85075e050578834f28c05e with
λ x0 x1 . TwoRamseyProp (ordsucc u2) (ordsucc u4) (ordsucc (ordsucc x0)).
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with
u2,
u4,
u8,
u4 leaving 4 subgoals.
The subproof is completed by applying nat_8.
The subproof is completed by applying nat_4.
The subproof is completed by applying TwoRamseyProp_3_4_9.
The subproof is completed by applying unknownprop_0b333a54acf90ac2cb68915649df7a73a736b590f76b23b6e0e8b35fbb9faf0c with
ordsucc u4.