Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: nat_p x0. Apply H0 with λ x1 . 0 ∈ ordsucc x1 leaving 2 subgoals. The subproof is completed by applying In_0_1. Let x1 of type ι be given. Assume H1: 0 ∈ ordsucc x1. Apply ordsuccI1 with ordsucc x1, 0. The subproof is completed by applying H1. ■