Apply unknownprop_aae4e03000d6619cc34e5a66244db6980d668b70bdfc22610af1046fd13449ea with
4,
8,
141,
prim4 8 leaving 2 subgoals.
Apply atleastp_tra with
141,
exp_nat 2 8,
prim4 8 leaving 2 subgoals.
Apply unknownprop_53a54314c9a6a892295b2ded3eab37435879a00813e71bc2836df12be576e7ac with
λ x0 x1 . atleastp 141 x1.
Apply nat_In_atleastp with
ChurchNum_ii_8 ChurchNum2 ordsucc 0,
141 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c39f4091a15f1ff7b3dd65d38fd37d060cdcbceda205863f5e715a04f6271f28.
The subproof is completed by applying unknownprop_3aee70737bb57b22447479b42793b9c5c341a5d14bd6a3d33ac700c4ce9f7bdd.
Apply equip_atleastp with
exp_nat 2 8,
prim4 8.
Apply equip_sym with
prim4 8,
exp_nat 2 8.
Apply unknownprop_f5822e9d5891900b4c653eab5e89c5bb71543e61fe2c332750489ecd340604eb with
8.
The subproof is completed by applying nat_8.
The subproof is completed by applying TwoRamseyProp_4_8_141.