Apply not_TwoRamseyProp_4_5_24.
Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
u4,
u5,
prim4 u4,
u24 leaving 2 subgoals.
Apply atleastp_tra with
prim4 u4,
u16,
u24 leaving 2 subgoals.
Apply equip_atleastp with
prim4 u4,
u16.
Apply unknownprop_18dab10013860d442d73fc2b55cfee57e61b2e3044d2d0c29767dba9e5eb2112 with
λ x0 x1 . equip (prim4 u4) x0.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with
4.
The subproof is completed by applying nat_4.
Apply nat_In_atleastp with
u24,
u16 leaving 2 subgoals.
The subproof is completed by applying unknownprop_a7f3578ada9cacf1cb3296f5290d2c691e8a6f96bb11bbe9193ef025e25fc69a.
Apply unknownprop_bf2b81e6403dbb816616ca5b741869e1f96c53bee8ce62b552a9a9320e0268db with
λ x0 x1 . u16 ∈ ordsucc x0.
Apply unknownprop_65854e80dcdfdaad216d9278c1826bfa6e412eacf7818f3d49e43d93a23f7bcf with
u16,
u7.
The subproof is completed by applying nat_7.
Apply unknownprop_8aec7aa3dfe2dc8cbf1366cb9f5d8ab2c4ceeb7b1cd3cc933b26d92d53269901 with
u4,
u5,
prim4 u4.
Apply TwoRamseyProp_atleastp_atleastp with
u5,
u4,
u5,
u5,
prim4 u4 leaving 3 subgoals.
The subproof is completed by applying H0.
Apply nat_In_atleastp with
u5,
u4 leaving 2 subgoals.
The subproof is completed by applying nat_5.
The subproof is completed by applying ordsuccI2 with
u4.
The subproof is completed by applying atleastp_ref with
u5.