Apply unknownprop_932963e4bf99485bf11d023ea4e4c5061a89d9d034de74ce451728ae15f94bee with
λ x0 x1 . TwoRamseyProp (ordsucc u3) (ordsucc u4) (ordsucc (ordsucc x0)).
Apply unknownprop_8dc90256cd485c4892a87cecdc3cbbfe0b65eb0964cbc26ac7da8ca72ab39534 with
u3,
u4,
u17,
u13 leaving 4 subgoals.
The subproof is completed by applying nat_17.
The subproof is completed by applying nat_13.
The subproof is completed by applying TwoRamseyProp_4_4_18.
The subproof is completed by applying TwoRamseyProp_3_5_14.