Let P be given.
Assume H1: ∀x y z, SNo x → SNo y → SNo z → (∀u ∈ SNoS_ (SNoLev x), P u y z) → (∀v ∈ SNoS_ (SNoLev y), P x v z) → (∀w ∈ SNoS_ (SNoLev z), P x y w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), P u v z) → (∀u ∈ SNoS_ (SNoLev x), ∀w ∈ SNoS_ (SNoLev z), P u y w) → (∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P x v w) → (∀u ∈ SNoS_ (SNoLev x), ∀v ∈ SNoS_ (SNoLev y), ∀w ∈ SNoS_ (SNoLev z), P u v w) → P x y z.
We prove the intermediate claim L1: ∀alpha, ordinal alpha → ∀beta, ordinal beta → ∀gamma, ordinal gamma → ∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ beta, ∀z ∈ SNoS_ gamma, P x y z.
Apply ordinal_ind to the current goal.
Let alpha be given.
Assume Ha: ordinal alpha.
Assume IHa: ∀delta ∈ alpha, ∀beta, ordinal beta → ∀gamma, ordinal gamma → ∀x ∈ SNoS_ delta, ∀y ∈ SNoS_ beta, ∀z ∈ SNoS_ gamma, P x y z.
Apply ordinal_ind to the current goal.
Let beta be given.
Assume Hb: ordinal beta.
Assume IHb: ∀delta ∈ beta, ∀gamma, ordinal gamma → ∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ delta, ∀z ∈ SNoS_ gamma, P x y z.
Apply ordinal_ind to the current goal.
Let gamma be given.
Assume Hc: ordinal gamma.
Assume IHc: ∀delta ∈ gamma, ∀x ∈ SNoS_ alpha, ∀y ∈ SNoS_ beta, ∀z ∈ SNoS_ delta, P x y z.
Let x be given.
Assume Hx: x ∈ SNoS_ alpha.
Let y be given.
Assume Hy: y ∈ SNoS_ beta.
Let z be given.
Assume Hz: z ∈ SNoS_ gamma.
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 SNoS_E2 gamma Hc z Hz to the current goal.
Assume Hz1: SNoLev z ∈ gamma.
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 beta Hb gamma 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 gamma 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 gamma 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 beta 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.
An exact proof term for the current goal is SNo_ordinal_ind3 P L1.
∎