Apply unknownprop_8f091fac19628539fcf2e218e3dc2a99ae1149b00810a44df3df9898ec6617fb with
ordsucc,
prim1,
ChurchNum_ii_3 ChurchNum2 ordsucc (ChurchNum_ii_2 ChurchNum2 ordsucc 100),
99 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_0a70d2d43ea31863dc5afb5c5dd839dddd16f01bbe480459e9d6b2402dd27bce with
ordsucc,
prim1,
ChurchNum_ii_2 ChurchNum2 ordsucc 100,
99 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_11e15fca8ff1d439d23914dd5828d3dfc7587cdbdb1b58f4cdcd37abbc83a41a with
ordsucc,
prim1,
100,
99 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
The subproof is completed by applying ordsuccI2 with 99.