Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: ordinal x0. Assume H1: ∀ x1 . nat_p x1 ⟶ add_nat x0 x1 = add_SNo x0 x1. Let x1 of type ι be given. Assume H2: x1 ∈ omega. Apply H1 with x1. Apply omega_nat_p with x1. The subproof is completed by applying H2. ■