Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
4,
7,
99,
prim4 7 leaving 2 subgoals.
Apply atleastp_tra with
99,
exp_nat 2 7,
prim4 7 leaving 2 subgoals.
Apply unknownprop_6df9254739f4a388867a5d36973fd227e06018cecfed76efdc871bfcb7b2c526 with
λ x0 x1 . atleastp 99 x1.
Apply nat_In_atleastp with
ChurchNum_ii_7 ChurchNum2 ordsucc 0,
99 leaving 2 subgoals.
The subproof is completed by applying unknownprop_6e53a236b7ea8e68ba2218da7e776817c8344b3c6935bc90e79d581ea505cdeb.
The subproof is completed by applying unknownprop_be16e914920ad073d26879063286969bc9cd22cf037ab8c703cb7b2b1b7ff149.
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_7_99.