Apply nat_ind with λ x0 . or (x0 = 0) (∃ x1 . and (nat_p x1) (x0 = ordsucc x1)) leaving 2 subgoals.

Apply orIL with 0 = 0, ∃ x0 . and (nat_p x0) (0 = ordsucc x0).

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

Assume H0: x0 0 0.

The subproof is completed by applying H0.

Let x0 of type ι be given.

Assume H0: nat_p x0.

Assume H1: or (x0 = 0) (∃ x1 . and (nat_p x1) (x0 = ordsucc x1)).

Apply orIR with ordsucc x0 = 0, ∃ x1 . and (nat_p x1) (ordsucc x0 = ordsucc x1).

Let x1 of type ο be given.

Assume H2: ∀ x2 . and (nat_p x2) (ordsucc x0 = ordsucc x2) ⟶ x1.

Apply H2 with x0.

Apply andI with nat_p x0, ordsucc x0 = ordsucc x0 leaving 2 subgoals.

The subproof is completed by applying H0.

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

Assume H3: x2 (ordsucc x0) (ordsucc x0).

The subproof is completed by applying H3.

■

Proofgold Proof