Apply unknownprop_af1ecdf9ce6b04278d3e4fc32870f99c200ac770476565e590e79cfb33806b67 with
ordsucc,
prim1,
ChurchNum_ii_4 ChurchNum2 ordsucc (ChurchNum_ii_3 ChurchNum2 ordsucc (ChurchNum_ii_2 ChurchNum2 ordsucc 68)),
66 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_8f091fac19628539fcf2e218e3dc2a99ae1149b00810a44df3df9898ec6617fb with
ordsucc,
prim1,
ChurchNum_ii_3 ChurchNum2 ordsucc (ChurchNum_ii_2 ChurchNum2 ordsucc 68),
66 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_0a70d2d43ea31863dc5afb5c5dd839dddd16f01bbe480459e9d6b2402dd27bce with
ordsucc,
prim1,
ChurchNum_ii_2 ChurchNum2 ordsucc 68,
66 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_11e15fca8ff1d439d23914dd5828d3dfc7587cdbdb1b58f4cdcd37abbc83a41a with
ordsucc,
prim1,
68,
66 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply ordsuccI1 with
67,
66.
The subproof is completed by applying ordsuccI2 with 66.