Let P be given.
Assume H1: ∀x y, SNo x → SNo y → (∀w ∈ SNoS_ (SNoLev x), P w y) → (∀z ∈ SNoS_ (SNoLev y), P x z) → (∀w ∈ SNoS_ (SNoLev x), ∀z ∈ SNoS_ (SNoLev y), P w z) → P x y.
We prove the intermediate claim L1: ∀α, ordinal α → ∀β, ordinal β → ∀x ∈ SNoS_ α, ∀y ∈ SNoS_ β, P x y.
Apply ordinal_ind to the current goal.
Let α be given.
Assume Ha: ordinal α.
Assume IHa: ∀γ ∈ α, ∀β, ordinal β → ∀x ∈ SNoS_ γ, ∀y ∈ SNoS_ β, P x y.
Apply ordinal_ind to the current goal.
Let β be given.
Assume Hb: ordinal β.
Assume IHb: ∀δ ∈ β, ∀x ∈ SNoS_ α, ∀y ∈ SNoS_ δ, P x y.
Let x be given.
Assume Hx: x ∈ SNoS_ α.
Let y be given.
Assume Hy: y ∈ 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 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 β 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.
An exact proof term for the current goal is SNo_ordinal_ind2 P L1.
∎