Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
3,
4,
11,
prim4 4 leaving 2 subgoals.
Apply atleastp_tra with
11,
16,
prim4 4 leaving 2 subgoals.
Apply nat_In_atleastp with
16,
11 leaving 2 subgoals.
The subproof is completed by applying nat_16.
The subproof is completed by applying unknownprop_ae3e46fe1608a88c13cfd94c7c4f636604e089dbe99822d5f16bc7323d0026af.
Apply equip_atleastp with
16,
prim4 4.
Apply equip_sym with
prim4 4,
16.
Apply unknownprop_18dab10013860d442d73fc2b55cfee57e61b2e3044d2d0c29767dba9e5eb2112 with
λ x0 x1 . equip (prim4 4) x0.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with
4.
The subproof is completed by applying nat_4.
The subproof is completed by applying TwoRamseyProp_3_4_11.