Let n be given.
Assume Hn.
We prove the intermediate claim Ln: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Ln2: ordinal n.
An exact proof term for the current goal is nat_p_ordinal n Ln.
We prove the intermediate claim L1: SNoS_ n = ⋃i ∈ n{x ∈ SNoS_ ω|SNoLev x = i}.
Apply set_ext to the current goal.
Let x be given.
Assume Hx.
Apply SNoS_E2 n Ln2 x Hx to the current goal.
Assume Hx1: SNoLev x ∈ n.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
Apply famunionI n (λi ⇒ {x ∈ SNoS_ ω|SNoLev x = i}) (SNoLev x) x Hx1 to the current goal.
We will prove x ∈ {x' ∈ SNoS_ ω|SNoLev x' = SNoLev x}.
Apply SepI to the current goal.
We will prove x ∈ SNoS_ ω.
Apply SNoS_Subq n ω Ln2 omega_ordinal to the current goal.
We will prove n ⊆ ω.
An exact proof term for the current goal is omega_TransSet n Hn.
An exact proof term for the current goal is Hx.
We will prove SNoLev x = SNoLev x.
Use reflexivity.
Let x be given.
Assume Hx.
Apply famunionE_impred n (λi ⇒ {x ∈ SNoS_ ω|SNoLev x = i}) x Hx to the current goal.
Let i be given.
Assume Hi: i ∈ n.
Assume H1.
Apply SepE (SNoS_ ω) (λx ⇒ SNoLev x = i) x H1 to the current goal.
Assume Hxa: x ∈ SNoS_ ω.
Assume Hxb: SNoLev x = i.
We will prove x ∈ SNoS_ n.
Apply SNoS_E2 ω omega_ordinal x Hxa 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_I n Ln2 x (SNoLev x) to the current goal.
We will prove SNoLev x ∈ n.
rewrite the current goal using Hxb (from left to right).
An exact proof term for the current goal is Hi.
We will prove SNo_ (SNoLev x) x.
An exact proof term for the current goal is Hx4.
rewrite the current goal using L1 (from left to right).
We will prove finite (⋃i ∈ n{x ∈ SNoS_ ω|SNoLev x = i}).
Apply famunion_nat_finite (λi ⇒ {x ∈ SNoS_ ω|SNoLev x = i}) n Ln to the current goal.
Let i be given.
Assume Hi: i ∈ n.
We will prove finite {x ∈ SNoS_ ω|SNoLev x = i}.
We will prove ∃m ∈ ω, equip {x ∈ SNoS_ ω|SNoLev x = i} m.
We use 2 ^ i to witness the existential quantifier.
Apply andI to the current goal.
We will prove 2 ^ i ∈ ω.
Apply nat_p_omega to the current goal.
An exact proof term for the current goal is nat_exp_SNo_nat 2 nat_2 i (nat_p_trans n Ln i Hi).
An exact proof term for the current goal is SNoS_omega_Lev_equip i (nat_p_trans n Ln i Hi).
∎