Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply beta with
omega,
λ x3 . nat_primrec x0 (λ x4 x5 . ap x1 x4) x3,
ordsucc x2,
λ x3 x4 . x4 = ap x1 x2 leaving 2 subgoals.
Apply omega_ordsucc with
x2.
The subproof is completed by applying H0.
Apply nat_primrec_S with
x0,
λ x3 x4 . ap x1 x3,
x2.
Apply omega_nat_p with
x2.
The subproof is completed by applying H0.