Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
4,
5,
41,
prim4 6 leaving 2 subgoals.
Apply atleastp_tra with
41,
exp_nat 2 6,
prim4 6 leaving 2 subgoals.
The subproof is completed by applying unknownprop_a2d5e99b6fe9290abe2cdc8190514e52008783dc6767ecd3bb7890e9d9df1cb8.
Apply equip_atleastp with
exp_nat 2 6,
prim4 6.
Apply equip_sym with
prim4 6,
exp_nat 2 6.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with
6.
The subproof is completed by applying nat_6.
The subproof is completed by applying TwoRamseyProp_4_5_41.