Proofgold Proof

pf
Let x0 of type ι → ο be given. Assume H0: x0 0. Assume H1: ∀ x1 . nat_p x1 ⟶ x0 (ordsucc x1). Apply nat_ind with λ x1 . x0 x1 leaving 2 subgoals. The subproof is completed by applying H0. Let x1 of type ι be given. Assume H2: nat_p x1. Assume H3: x0 x1. Apply H1 with x1. The subproof is completed by applying H2. ■