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