Proofgold Proof

pf
Let x0 of type ι be given. Assume H0: x0 ∈ omega. Apply binunionI2 with omega, {minus_SNo x1\|x1 ∈ omega}, minus_SNo x0. Apply ReplI with omega, minus_SNo, x0. The subproof is completed by applying H0. ■