Let x be given.

Assume Hx: SNo x.

Set alpha to be the term SNoLev x.

We prove the intermediate claim La: ordinal alpha.

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

We will prove SNoEq_ alpha (SNo_extend1 x) x.

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

Set q to be the term λbeta ⇒ beta ∈ x ∨ beta = alpha of type set → prop.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) p.

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

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q.

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

We will prove PNoEq_ (ordsucc alpha) (λbeta ⇒ beta ∈ PSNo (ordsucc alpha) q) q.

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

We will prove PNoEq_ alpha q p.

Apply PNoEq_sym_ to the current goal.

An exact proof term for the current goal is PNo_extend1_eq alpha p.

∎