Apply nat_ind with λ x0 . add_nat 0 x0 = x0 leaving 2 subgoals.

The subproof is completed by applying add_nat_0R with 0.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: add_nat 0 x0 = x0.

Apply add_nat_SR with 0, x0, λ x1 x2 . x2 = ordsucc x0 leaving 2 subgoals.

The subproof is completed by applying H0.

Apply H1 with λ x1 x2 . ordsucc x2 = ordsucc x0.

Let x1 of type ι → ι → ο be given.

Assume H2: x1 (ordsucc x0) (ordsucc x0).

The subproof is completed by applying H2.

■

Proofgold Proof