Let x0 of type (ι → ι) → ι → ι be given.
Apply H0 with
λ x1 : (ι → ι) → ι → ι . nat_p (x1 ordsucc 0) leaving 2 subgoals.
The subproof is completed by applying nat_0.
Let x1 of type (ι → ι) → ι → ι be given.
Apply nat_ordsucc with
x1 ordsucc 0.
The subproof is completed by applying H1.