Let z be given.
Assume Hz.
Apply HSNo_E z Hz to the current goal.
Let x and y be given.
Assume Hx: CSNo x.
Assume Hy: CSNo y.
Assume Hzxy: z = CSNo_pair x y.
Let v be given.
Assume Hv: v ∈ ⋃ (CSNo_pair x y).
Apply UnionE_impred (CSNo_pair x y) v Hv to the current goal.
Let u be given.
Assume H1: v ∈ u.
Assume H2: u ∈ CSNo_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 ∈ 4, v = {i}.
An exact proof term for the current goal is extension_SNoElt_mon 3 4 (ordsuccI1 3) x (CSNo_ExtendedSNoElt_3 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 {{3}} 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 3 4 (ordsuccI1 3) y (CSNo_ExtendedSNoElt_3 y Hy) v L3.
Assume H5: v ∈ {{3}}.
We will prove ordinal v ∨ ∃i ∈ 4, v = {i}.
Apply orIR to the current goal.
We use 3 to witness the existential quantifier.
Apply andI to the current goal.
We will prove 3 ∈ 4.
An exact proof term for the current goal is In_3_4.
We will prove v = {3}.
An exact proof term for the current goal is SingE {3} v H5.
∎