Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
3,
9,
51,
prim4 6 leaving 2 subgoals.
Apply atleastp_tra with
51,
exp_nat 2 6,
prim4 6 leaving 2 subgoals.
Apply unknownprop_180b0fd5c0d77d89fc7c74d0519e38ad47b1b50cde73428ffe5103966c8941b7 with
λ x0 x1 . atleastp 51 x1.
Apply nat_In_atleastp with
ChurchNum_ii_6 ChurchNum2 ordsucc 0,
51 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c00f2f77a9de84adbe221e2db786f0dbccd295ee08ec6eb8eaaf0b0a862ad5bd.
The subproof is completed by applying unknownprop_2b48c4387a307967ffb3c866d71572d312c231203e7cfff6cc08843a1851bf8c.
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_3_9_51.