Apply unknownprop_44e0ba05d0717b02d304ea93cace392f852a965609b181bd83e00caede8a9540 with
ordsucc,
prim1,
ChurchNum_ii_5 ChurchNum2 ordsucc (ChurchNum_ii_3 ChurchNum2 ordsucc 152),
150 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_af1ecdf9ce6b04278d3e4fc32870f99c200ac770476565e590e79cfb33806b67 with
ordsucc,
prim1,
ChurchNum_ii_3 ChurchNum2 ordsucc 152,
150 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_0a70d2d43ea31863dc5afb5c5dd839dddd16f01bbe480459e9d6b2402dd27bce with
ordsucc,
prim1,
152,
150 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply ordsuccI1 with
151,
150.
The subproof is completed by applying ordsuccI2 with 150.