Apply unknownprop_44e0ba05d0717b02d304ea93cace392f852a965609b181bd83e00caede8a9540 with
ordsucc,
prim1,
ChurchNum_ii_5 ChurchNum2 ordsucc (ChurchNum_ii_4 ChurchNum2 ordsucc (ChurchNum2 ordsucc 142)),
141 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_af1ecdf9ce6b04278d3e4fc32870f99c200ac770476565e590e79cfb33806b67 with
ordsucc,
prim1,
ChurchNum_ii_4 ChurchNum2 ordsucc (ChurchNum2 ordsucc 142),
141 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_8f091fac19628539fcf2e218e3dc2a99ae1149b00810a44df3df9898ec6617fb with
ordsucc,
prim1,
ChurchNum2 ordsucc 142,
141 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
Apply unknownprop_652c33d51786d83ad73a9f3ad061b0312e77991db52346310444b921b4facd5f with
ordsucc,
prim1,
142,
141 leaving 2 subgoals.
The subproof is completed by applying ordsuccI1.
The subproof is completed by applying ordsuccI2 with 141.