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