Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

We prove the intermediate claim La: ordinal α.

An exact proof term for the current goal is SNoLev_ordinal x Hx.

We will prove SNoEq_ α (SNo_extend0 x) x.

Set p to be the term λβ ⇒ β ∈ x of type set → prop.

Set q to be the term λβ ⇒ β ∈ x ∧ β ≠ α of type set → prop.

We will prove PNoEq_ α (λβ ⇒ β ∈ PSNo (ordsucc α) q) p.

Apply PNoEq_tra_ α (λβ ⇒ β ∈ PSNo (ordsucc α) q) q p to the current goal.

We will prove PNoEq_ α (λβ ⇒ β ∈ PSNo (ordsucc α) q) q.

Apply PNoEq_antimon_ (λβ ⇒ β ∈ PSNo (ordsucc α) q) q (ordsucc α) (ordinal_ordsucc α La) α (ordsuccI2 α) to the current goal.

We will prove PNoEq_ (ordsucc α) (λβ ⇒ β ∈ PSNo (ordsucc α) q) q.

An exact proof term for the current goal is PNoEq_PSNo (ordsucc α) (ordinal_ordsucc α La) q.

We will prove PNoEq_ α q p.

Apply PNoEq_sym_ to the current goal.

An exact proof term for the current goal is PNo_extend0_eq α p.

∎