Apply unknownprop_0a70d2d43ea31863dc5afb5c5dd839dddd16f01bbe480459e9d6b2402dd27bce with
ordsucc,
prim1,
ChurchNum_ii_2 ChurchNum2 ordsucc 52,
51 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_11e15fca8ff1d439d23914dd5828d3dfc7587cdbdb1b58f4cdcd37abbc83a41a with
ordsucc,
prim1,
52,
51 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
The subproof is completed by applying ordsuccI2 with 51.