Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: nat_p x0. Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with ordsucc x0. Apply unknownprop_077979b790f9097ea9250573e60509ec9410103c35a67e0558983ee18582fb09 with x0. The subproof is completed by applying H0. ■