Apply int_SNo_cases with λ x0 . ∀ x1 : ο . (∀ x2 . x2 ∈ omega ⟶ x0 = minus_SNo (ordsucc x2) ⟶ x1) ⟶ (x0 = 0 ⟶ x1) ⟶ (∀ x2 . x2 ∈ omega ⟶ x0 = ordsucc x2 ⟶ x1) ⟶ x1 leaving 2 subgoals.

Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ο be given.

Assume H1: ∀ x2 . x2 ∈ omega ⟶ x0 = minus_SNo (ordsucc x2) ⟶ x1.

Assume H2: x0 = 0 ⟶ x1.

Assume H3: ∀ x2 . x2 ∈ omega ⟶ x0 = ordsucc x2 ⟶ x1.

Apply nat_inv_impred with λ x2 . x0 = x2 ⟶ x1, x0 leaving 4 subgoals.

The subproof is completed by applying H2.

Let x2 of type ι be given.

Assume H4: nat_p x2.

Apply H3 with x2.

Apply nat_p_omega with x2.

The subproof is completed by applying H4.

Apply omega_nat_p with x0.

The subproof is completed by applying H0.

Let x2 of type ι → ι → ο be given.

Assume H4: x2 x0 x0.

The subproof is completed by applying H4.

Let x0 of type ι be given.

Assume H0: x0 ∈ omega.

Let x1 of type ο be given.

Assume H1: ∀ x2 . x2 ∈ omega ⟶ minus_SNo x0 = minus_SNo (ordsucc x2) ⟶ x1.

Assume H2: minus_SNo x0 = 0 ⟶ x1.

Assume H3: ∀ x2 . x2 ∈ omega ⟶ minus_SNo x0 = ordsucc x2 ⟶ x1.

Apply nat_inv_impred with λ x2 . x0 = x2 ⟶ x1, x0 leaving 4 subgoals.

Assume H4: x0 = 0.

Apply H2.

Apply H4 with λ x2 x3 . minus_SNo x3 = 0.

The subproof is completed by applying minus_SNo_0.

Let x2 of type ι be given.

Assume H4: nat_p x2.

Assume H5: x0 = ordsucc x2.

Apply H1 with x2 leaving 2 subgoals.

Apply nat_p_omega with x2.

The subproof is completed by applying H4.

set y3 to be minus_SNo (ordsucc x2)

Claim L6: ∀ x4 : ι → ο . x4 y3 ⟶ x4 (minus_SNo x0)

Let x4 of type ι → ο be given.

The subproof is completed by applying H5 with λ x5 x6 . (λ x7 . x4) (minus_SNo x5) (minus_SNo x6).

Let x4 of type ι → ι → ο be given.

Apply L6 with λ x5 . x4 x5 y3 ⟶ x4 y3 x5.

Assume H7: x4 y3 y3.

The subproof is completed by applying H7.

Apply omega_nat_p with x0.

The subproof is completed by applying H0.

Let x2 of type ι → ι → ο be given.

Assume H4: x2 x0 x0.

The subproof is completed by applying H4.

■

Proofgold Proof