Let u be given.

Assume Hu: u ∈ PSNo alpha p.

We will prove u ∈ SNoElts_ alpha.

Apply binunionE {beta ∈ alpha|p beta} {beta '|beta ∈ alpha, ¬ p beta} u Hu to the current goal.

Assume H1: u ∈ {beta ∈ alpha|p beta}.

Apply SepE alpha p u H1 to the current goal.

Assume H2: u ∈ alpha.

Assume H3: p u.

We will prove u ∈ alpha ∪ {beta '|beta ∈ alpha}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is H2.

Assume H1: u ∈ {beta '|beta ∈ alpha, ¬ p beta}.

Apply ReplSepE_impred alpha (λbeta ⇒ ¬ p beta) (λbeta ⇒ beta ') u H1 to the current goal.

Let beta be given.

Assume H2: beta ∈ alpha.

Assume H3: ¬ p beta.

Assume H4: u = beta '.

We will prove u ∈ alpha ∪ {beta '|beta ∈ alpha}.

Apply binunionI2 to the current goal.

We will prove u ∈ {beta '|beta ∈ alpha}.

rewrite the current goal using H4 (from left to right).

An exact proof term for the current goal is ReplI alpha (λbeta ⇒ beta ') beta H2.

Let beta be given.

Assume H1: beta ∈ alpha.

We prove the intermediate claim Lbeta: ordinal beta.

An exact proof term for the current goal is ordinal_Hered alpha Ha beta H1.

We will prove exactly1of2 (beta ' ∈ PSNo alpha p) (beta ∈ PSNo alpha p).

Apply xm (p beta) to the current goal.

Assume H2: p beta.

Apply exactly1of2_I2 to the current goal.

We will prove beta ' ∉ PSNo alpha p.

Assume H3: beta ' ∈ PSNo alpha p.

Apply binunionE {beta ∈ alpha|p beta} {beta '|beta ∈ alpha, ¬ p beta} (beta ') H3 to the current goal.

Assume H4: beta ' ∈ {beta ∈ alpha|p beta}.

Apply SepE alpha p (beta ') H4 to the current goal.

Assume H5: beta ' ∈ alpha.

Assume H6: p (beta ').

We will prove False.

Apply tagged_not_ordinal beta to the current goal.

An exact proof term for the current goal is ordinal_Hered alpha Ha (beta ') H5.

Assume H4: beta ' ∈ {beta '|beta ∈ alpha, ¬ p beta}.

Apply ReplSepE_impred alpha (λbeta ⇒ ¬ p beta) (λbeta ⇒ beta ') (beta ') H4 to the current goal.

Let gamma be given.

Assume H5: gamma ∈ alpha.

Assume H6: ¬ p gamma.

Assume H7: beta ' = gamma '.

We prove the intermediate claim Lgamma: ordinal gamma.

An exact proof term for the current goal is ordinal_Hered alpha Ha gamma H5.

We prove the intermediate claim L1: beta = gamma.

An exact proof term for the current goal is tagged_eqE_eq beta gamma Lbeta Lgamma H7.

Apply H6 to the current goal.

We will prove p gamma.

rewrite the current goal using L1 (from right to left).

We will prove p beta.

An exact proof term for the current goal is H2.

We will prove beta ∈ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is SepI alpha p beta H1 H2.

Assume H2: ¬ p beta.

Apply exactly1of2_I1 to the current goal.

We will prove beta ' ∈ {beta ∈ alpha|p beta} ∪ {beta '|beta ∈ alpha, ¬ p beta}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplSepI alpha (λbeta ⇒ ¬ p beta) (λbeta ⇒ beta ') beta H1 H2.

We will prove beta ∉ PSNo alpha p.

Assume H3: beta ∈ PSNo alpha p.

Apply binunionE {beta ∈ alpha|p beta} {beta '|beta ∈ alpha, ¬ p beta} beta H3 to the current goal.

Assume H4: beta ∈ {beta ∈ alpha|p beta}.

Apply SepE alpha p beta H4 to the current goal.

Assume H5: beta ∈ alpha.

Assume H6: p beta.

We will prove False.

An exact proof term for the current goal is H2 H6.

Assume H4: beta ∈ {beta '|beta ∈ alpha, ¬ p beta}.

Apply ReplSepE_impred alpha (λbeta ⇒ ¬ p beta) (λbeta ⇒ beta ') beta H4 to the current goal.

Let gamma be given.

Assume H5: gamma ∈ alpha.

Assume H6: ¬ p gamma.

Assume H7: beta = gamma '.

Apply tagged_not_ordinal gamma to the current goal.

We will prove ordinal (gamma ').

rewrite the current goal using H7 (from right to left).

An exact proof term for the current goal is Lbeta.