Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: nat_p x0.

Let x1 of type ι → ο be given.

Assume H1: x1 0.

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

Apply nat_ind with x1, x0 leaving 3 subgoals.

The subproof is completed by applying H1.

Let x2 of type ι be given.

Assume H3: nat_p x2.

Assume H4: x1 x2.

Apply H2 with x2.

The subproof is completed by applying H3.

The subproof is completed by applying H0.

■