Proofgold Proof

pf

Let x0 of type ι be given.

Assume H0: SNo x0.

Let x1 of type ι be given.

Assume H1: x1 ∈ omega.

Let x2 of type ι be given.

Assume H2: x2 ∈ omega.

Apply exp_SNo_nat_mul_add with x0, x1, x2 leaving 3 subgoals.

The subproof is completed by applying H0.

Apply omega_nat_p with x1.

The subproof is completed by applying H1.

Apply omega_nat_p with x2.

The subproof is completed by applying H2.

■