Apply ordinal_ind to the current goal.

Let α be given.

Assume Ha: ordinal α.

Assume IHa: ∀δ ∈ α, ∀β, ordinal β → ∀γ, ordinal γ → ∀x ∈ SNoS_ δ, ∀y ∈ SNoS_ β, ∀z ∈ SNoS_ γ, P x y z.

Apply ordinal_ind to the current goal.

Let β be given.

Assume Hb: ordinal β.

Assume IHb: ∀δ ∈ β, ∀γ, ordinal γ → ∀x ∈ SNoS_ α, ∀y ∈ SNoS_ δ, ∀z ∈ SNoS_ γ, P x y z.

Apply ordinal_ind to the current goal.

Let γ be given.

Assume Hc: ordinal γ.

Assume IHc: ∀δ ∈ γ, ∀x ∈ SNoS_ α, ∀y ∈ SNoS_ β, ∀z ∈ SNoS_ δ, P x y z.

Let x be given.

Assume Hx: x ∈ SNoS_ α.

Let y be given.

Assume Hy: y ∈ SNoS_ β.

Let z be given.

Assume Hz: z ∈ SNoS_ γ.

Apply SNoS_E2 α Ha x Hx to the current goal.

Assume Hx1: SNoLev x ∈ α.

Assume Hx2: ordinal (SNoLev x).

Assume Hx3: SNo x.

Assume Hx4: SNo_ (SNoLev x) x.

Apply SNoS_E2 β Hb y Hy to the current goal.

Assume Hy1: SNoLev y ∈ β.

Assume Hy2: ordinal (SNoLev y).

Assume Hy3: SNo y.

Assume Hy4: SNo_ (SNoLev y) y.

Apply SNoS_E2 γ Hc z Hz to the current goal.

Assume Hz1: SNoLev z ∈ γ.

Assume Hz2: ordinal (SNoLev z).

Assume Hz3: SNo z.

Assume Hz4: SNo_ (SNoLev z) z.

Apply H1 x y z Hx3 Hy3 Hz3 to the current goal.

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

Let u be given.

Assume Hu: u ∈ SNoS_ (SNoLev x).

An exact proof term for the current goal is IHa (SNoLev x) Hx1 β Hb γ Hc u Hu y Hy z Hz.

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

Let v be given.

Assume Hv: v ∈ SNoS_ (SNoLev y).

An exact proof term for the current goal is IHb (SNoLev y) Hy1 γ Hc x Hx v Hv z Hz.

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

An exact proof term for the current goal is IHc (SNoLev z) Hz1 x Hx y Hy.

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

Let u be given.

Assume Hu: u ∈ SNoS_ (SNoLev x).

Let v be given.

Assume Hv: v ∈ SNoS_ (SNoLev y).

An exact proof term for the current goal is IHa (SNoLev x) Hx1 (SNoLev y) Hy2 γ Hc u Hu v Hv z Hz.

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

Let u be given.

Assume Hu: u ∈ SNoS_ (SNoLev x).

Let w be given.

Assume Hw: w ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is IHa (SNoLev x) Hx1 β Hb (SNoLev z) Hz2 u Hu y Hy w Hw.

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

Let v be given.

Assume Hv: v ∈ SNoS_ (SNoLev y).

Let w be given.

Assume Hw: w ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is IHb (SNoLev y) Hy1 (SNoLev z) Hz2 x Hx v Hv w Hw.

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

Let u be given.

Assume Hu: u ∈ SNoS_ (SNoLev x).

Let v be given.

Assume Hv: v ∈ SNoS_ (SNoLev y).

Let w be given.

Assume Hw: w ∈ SNoS_ (SNoLev z).

An exact proof term for the current goal is IHa (SNoLev x) Hx1 (SNoLev y) Hy2 (SNoLev z) Hz2 u Hu v Hv w Hw.