Let n be given.
Assume Hn.
Let x be given.
Assume Hx1: x ∈ SNoS_ (ordsucc n).
Assume Hx2: 0 < x.
Assume Hx3: SNoEq_ (SNoLev x) (eps_ n) x.
Apply SNoS_E2 (ordsucc n) (nat_p_ordinal (ordsucc n) (nat_ordsucc n Hn)) x Hx1 to the current goal.
Assume Hx1a: SNoLev x ∈ ordsucc n.
Assume Hx1b: ordinal (SNoLev x).
Assume Hx1c: SNo x.
Assume Hx1d: SNo_ (SNoLev x) x.
We prove the intermediate claim L1: nat_p (SNoLev x).
Apply nat_p_trans (ordsucc n) (nat_ordsucc n Hn) to the current goal.
We will prove SNoLev x ∈ ordsucc n.
An exact proof term for the current goal is Hx1a.
Apply nat_inv (SNoLev x) L1 to the current goal.
Assume H1: SNoLev x = 0.
We will prove False.
We prove the intermediate claim L2: x = 0.
An exact proof term for the current goal is SNoLev_0_eq_0 x Hx1c H1.
Apply SNoLt_irref x to the current goal.
rewrite the current goal using L2 (from left to right) at position 1.
An exact proof term for the current goal is Hx2.
Assume H1.
Apply H1 to the current goal.
Let m be given.
Assume H1.
Apply H1 to the current goal.
Assume Hm1: nat_p m.
Assume Hm2: SNoLev x = ordsucc m.
We use m to witness the existential quantifier.
Apply andI to the current goal.
We will prove m ∈ n.
Apply nat_ordsucc_trans n Hn (SNoLev x) Hx1a to the current goal.
We will prove m ∈ SNoLev x.
rewrite the current goal using Hm2 (from left to right).
Apply ordsuccI2 to the current goal.
We will prove x = eps_ m.
Apply SNo_eq x (eps_ m) Hx1c (SNo_eps_ m (nat_p_omega m Hm1)) to the current goal.
We will prove SNoLev x = SNoLev (eps_ m).
rewrite the current goal using SNoLev_eps_ m (nat_p_omega m Hm1) (from left to right).
An exact proof term for the current goal is Hm2.
We will prove SNoEq_ (SNoLev x) x (eps_ m).
Apply SNoEq_tra_ (SNoLev x) x (eps_ n) (eps_ m) to the current goal.
Apply SNoEq_sym_ to the current goal.
An exact proof term for the current goal is Hx3.
We will prove SNoEq_ (SNoLev x) (eps_ n) (eps_ m).
rewrite the current goal using Hm2 (from left to right).
We will prove SNoEq_ (ordsucc m) (eps_ n) (eps_ m).
Apply SNoEq_I to the current goal.
Let k be given.
Assume Hk: k ∈ ordsucc m.
We prove the intermediate claim L3: ordinal k.
An exact proof term for the current goal is nat_p_ordinal k (nat_p_trans (ordsucc m) (nat_ordsucc m Hm1) k Hk).
Apply iffI to the current goal.
Assume H2: k ∈ eps_ n.
rewrite the current goal using eps_ordinal_In_eq_0 n k L3 H2 (from left to right).
We will prove 0 ∈ eps_ m.
We will prove 0 ∈ {0} ∪ {SetAdjoin (ordsucc k) {1}|k ∈ m}.
Apply binunionI1 to the current goal.
Apply SingI to the current goal.
Assume H2: k ∈ eps_ m.
rewrite the current goal using eps_ordinal_In_eq_0 m k L3 H2 (from left to right).
We will prove 0 ∈ eps_ n.
We will prove 0 ∈ {0} ∪ {SetAdjoin (ordsucc k) {1}|k ∈ n}.
Apply binunionI1 to the current goal.
Apply SingI to the current goal.
∎