Apply unknownprop_25e71d8a7ad20837122ea1d4ff51220449571353b61bd172f7ce85161686ccac with
ordsucc,
nat_p,
λ x0 . add_nat 41 x0,
ChurchNum_ii_3 ChurchNum2 ordsucc 0,
λ x0 x1 . x1 = 65 leaving 4 subgoals.
The subproof is completed by applying nat_ordsucc.
The subproof is completed by applying add_nat_SR with 41.
The subproof is completed by applying nat_8.
Apply unknownprop_e2cb0de7874d400d74b6cb5cf619af6f48ae813f369fbf388b00f41ca04e606a with
ordsucc,
nat_p,
λ x0 . add_nat 41 x0,
0,
λ x0 x1 . ChurchNum_ii_4 ChurchNum2 ordsucc x1 = 65 leaving 4 subgoals.
The subproof is completed by applying nat_ordsucc.
The subproof is completed by applying add_nat_SR with 41.
The subproof is completed by applying nat_0.