Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
u5,
u5,
u64,
prim4 u6 leaving 2 subgoals.
Apply unknownprop_4d619f8c0c4edc98bd8e6be92366236784a59ad7862cae98bda091f9d44c9792 with
λ x0 x1 . atleastp x0 (prim4 u6).
Apply equip_atleastp with
exp_nat u2 u6,
prim4 u6.
Apply equip_sym with
prim4 u6,
exp_nat u2 u6.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with
u6.
The subproof is completed by applying nat_6.
The subproof is completed by applying TwoRamseyProp_u5_u5_u64.