Let z be given.
Assume Hz.
Apply CSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hzxy: z = SNo_pair x y.
Let v be given.
Assume Hv: v ∈ ⋃ (SNo_pair x y).
Apply UnionE_impred (SNo_pair x y) v Hv to the current goal.
Let u be given.
Assume H1: v ∈ u.
Assume H2: u ∈ SNo_pair x y.
Apply binunionE x {w ''|w ∈ y} u H2 to the current goal.
Assume H3: u ∈ x.
We prove the intermediate claim L1: v ∈ ⋃ x.
An exact proof term for the current goal is UnionI x v u H1 H3.
We will prove ordinal v ∨ ∃i ∈ 3, v = {i}.
An exact proof term for the current goal is extension_SNoElt_mon 2 3 (ordsuccI1 2) x (SNo_ExtendedSNoElt_2 x Hx) v L1.
Assume H3: u ∈ {w ''|w ∈ y}.
Apply ReplE_impred y ctag u H3 to the current goal.
Let w be given.
Assume Hw: w ∈ y.
Assume H4: u = w ''.
We prove the intermediate claim L2: v ∈ w ''.
rewrite the current goal using H4 (from right to left).
An exact proof term for the current goal is H1.
Apply binunionE w {{2}} v L2 to the current goal.
Assume H5: v ∈ w.
We prove the intermediate claim L3: v ∈ ⋃ y.
An exact proof term for the current goal is UnionI y v w H5 Hw.
An exact proof term for the current goal is extension_SNoElt_mon 2 3 (ordsuccI1 2) y (SNo_ExtendedSNoElt_2 y Hy) v L3.
Assume H5: v ∈ {{2}}.
We will prove ordinal v ∨ ∃i ∈ 3, v = {i}.
Apply orIR to the current goal.
We use 2 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 2 ∈ 3.
An exact proof term for the current goal is In_2_3.
We will prove v = {2}.
An exact proof term for the current goal is SingE {2} v H5.
∎