Apply ordinal_ind to the current goal.

Let alpha be given.

Assume Ha: ordinal alpha.

Assume IHa: ∀gamma ∈ alpha, ∀beta, ordinal beta → ∀x ∈ SNoS_ gamma, ∀y ∈ SNoS_ beta, P x y.

Apply ordinal_ind to the current goal.

Let beta be given.

Assume Hb: ordinal beta.

Assume IHb: ∀delta ∈ beta, ∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ delta, P x y.

Let x be given.

Assume Hx: x ∈ SNoS_ alpha.

Let y be given.

Assume Hy: y ∈ SNoS_ beta.

Apply SNoS_E2 alpha Ha x Hx to the current goal.

Assume Hx1: SNoLev x ∈ alpha.

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

Apply SNoS_E2 beta Hb y Hy to the current goal.

Assume Hy1: SNoLev y ∈ beta.

Assume Hy2: ordinal (SNoLev y).

Assume Hy3: SNo y.

Assume Hy4: SNo_ (SNoLev y) y.

Apply H1 x y Hx3 Hy3 to the current goal.

We will prove ∀w ∈ SNoS_ (SNoLev x), P w y.

Let w be given.

Assume Hw: w ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is IHa (SNoLev x) Hx1 beta Hb w Hw y Hy.

We will prove ∀z ∈ SNoS_ (SNoLev y), P x z.

An exact proof term for the current goal is IHb (SNoLev y) Hy1 x Hx.

We will prove ∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), P w z.

Let w be given.

Assume Hw: w ∈ SNoS_ (SNoLev x).

Let z be given.

Assume Hz: z ∈ SNoS_ (SNoLev y).

An exact proof term for the current goal is IHa (SNoLev x) Hx1 (SNoLev y) Hy2 w Hw z Hz.