Let x be given.
Assume Hx.
Let v be given.
Assume Hv.
We will prove ordinal v ∨ ∃i ∈ 2, v = {i}.
Apply UnionE_impred x v Hv to the current goal.
Let u be given.
Assume H1: v ∈ u.
Assume H2: u ∈ x.
Apply SNoLev_ x Hx to the current goal.
Assume H3: x ⊆ SNoElts_ (SNoLev x).
Assume _.
Apply binunionE (SNoLev x) {beta '|beta ∈ SNoLev x} u (H3 u H2) to the current goal.
Assume H4: u ∈ SNoLev x.
We prove the intermediate claim Luo: ordinal u.
An exact proof term for the current goal is ordinal_Hered (SNoLev x) (SNoLev_ordinal x Hx) u H4.
We will prove ordinal v ∨ ∃i ∈ 2, v = {i}.
Apply orIL to the current goal.
An exact proof term for the current goal is ordinal_Hered u Luo v H1.
Assume H4: u ∈ {beta '|beta ∈ SNoLev x}.
Apply ReplE_impred (SNoLev x) tag u H4 to the current goal.
Let beta be given.
Assume Hb: beta ∈ SNoLev x.
Assume Hub: u = beta '.
We prove the intermediate claim Lv: v ∈ beta '.
rewrite the current goal using Hub (from right to left).
An exact proof term for the current goal is H1.
Apply binunionE beta {{1}} v Lv to the current goal.
Assume H5: v ∈ beta.
We prove the intermediate claim Lbo: ordinal beta.
An exact proof term for the current goal is ordinal_Hered (SNoLev x) (SNoLev_ordinal x Hx) beta Hb.
We will prove ordinal v ∨ ∃i ∈ 2, v = {i}.
Apply orIL to the current goal.
An exact proof term for the current goal is ordinal_Hered beta Lbo v H5.
Assume H5: v ∈ {{1}}.
We will prove ordinal v ∨ ∃i ∈ 2, v = {i}.
Apply orIR to the current goal.
We use 1 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is In_1_2.
We will prove v = {1}.
An exact proof term for the current goal is SingE {1} v H5.
∎