Apply unknownprop_3d492f63bbda05786f59e1a020a0f00cded12b012672cfcb59b4dfe595a76487 with
ordsucc,
nat_p,
λ x0 . add_nat 66 x0,
0,
λ x0 x1 . x1 = 98 leaving 4 subgoals.
The subproof is completed by applying nat_ordsucc.
The subproof is completed by applying add_nat_SR with 66.
The subproof is completed by applying nat_0.
Apply add_nat_0R with
66,
λ x0 x1 . ChurchNum_ii_5 ChurchNum2 ordsucc x1 = 98.
Let x0 of type ι → ι → ο be given.
The subproof is completed by applying H0.