Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
4,
6,
66,
prim4 7 leaving 2 subgoals.
Apply atleastp_tra with
66,
exp_nat 2 7,
prim4 7 leaving 2 subgoals.
Apply unknownprop_6df9254739f4a388867a5d36973fd227e06018cecfed76efdc871bfcb7b2c526 with
λ x0 x1 . atleastp 66 x1.
Apply nat_In_atleastp with
ChurchNum_ii_7 ChurchNum2 ordsucc 0,
66 leaving 2 subgoals.
The subproof is completed by applying unknownprop_6e53a236b7ea8e68ba2218da7e776817c8344b3c6935bc90e79d581ea505cdeb.
The subproof is completed by applying unknownprop_384212a15605fec6985c8c13806539a9c8c7cd5133b06cbd51d7b59e1d5deb0a.
Apply equip_atleastp with
exp_nat 2 7,
prim4 7.
Apply equip_sym with
prim4 7,
exp_nat 2 7.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with
7.
The subproof is completed by applying nat_7.
The subproof is completed by applying TwoRamseyProp_4_6_66.