Apply SNoLev_ordinal x to the current goal.

An exact proof term for the current goal is Hx.

Apply SNoLev_ordinal y to the current goal.

An exact proof term for the current goal is Hy.

Assume H1: PNoLt_ (SNoLev x ∩ SNoLev y) (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y).

Apply PNoLt_E_ (SNoLev x ∩ SNoLev y) (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) H1 to the current goal.

Let alpha be given.

Assume Ha: alpha ∈ SNoLev x ∩ SNoLev y.

Assume H2: PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y).

Assume H3: alpha ∉ x.

Assume H4: alpha ∈ y.

Apply binintersectE (SNoLev x) (SNoLev y) alpha Ha to the current goal.

Assume Ha1: alpha ∈ SNoLev x.

Assume Ha2: alpha ∈ SNoLev y.

We prove the intermediate claim La: ordinal alpha.

An exact proof term for the current goal is ordinal_Hered (SNoLev x) LLx alpha Ha1.

Set z to be the term PSNo alpha (λbeta ⇒ beta ∈ x).

We prove the intermediate claim L1: SNo_ alpha z.

Apply SNo_PSNo to the current goal.

An exact proof term for the current goal is La.

We prove the intermediate claim L2: SNo z.

We will prove ∃alpha, ordinal alpha ∧ SNo_ alpha z.

We use alpha to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is La.

An exact proof term for the current goal is L1.

Apply SNoLev_prop z L2 to the current goal.

Assume Hz1: ordinal (SNoLev z).

Assume Hz2: SNo_ (SNoLev z) z.

We prove the intermediate claim L3: SNoLev z = alpha.

An exact proof term for the current goal is SNoLev_uniq z (SNoLev z) alpha Hz1 La Hz2 L1.

We prove the intermediate claim L4: SNoEq_ alpha z x.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ z) (λbeta ⇒ beta ∈ x).

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

Apply PNoEq_PSNo to the current goal.

An exact proof term for the current goal is La.

We prove the intermediate claim L5: SNoEq_ alpha z y.

Apply SNoEq_tra_ alpha z x y L4 to the current goal.

We will prove SNoEq_ alpha x y.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y).

An exact proof term for the current goal is H2.

Apply Hp1 z L2 to the current goal.

We will prove SNoLev z ∈ SNoLev x ∩ SNoLev y.

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

An exact proof term for the current goal is Ha.

We will prove SNoEq_ (SNoLev z) z x.

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

An exact proof term for the current goal is L4.

We will prove SNoEq_ (SNoLev z) z y.

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

An exact proof term for the current goal is L5.

We will prove x < z.

We will prove PNoLt (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev z) (λbeta ⇒ beta ∈ z).

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

We will prove PNoLt (SNoLev x) (λbeta ⇒ beta ∈ x) alpha (λbeta ⇒ beta ∈ z).

Apply PNoLtI3 to the current goal.

We will prove alpha ∈ SNoLev x.

An exact proof term for the current goal is Ha1.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ z).

Apply PNoEq_sym_ to the current goal.

An exact proof term for the current goal is L4.

We will prove alpha ∉ x.

An exact proof term for the current goal is H3.

We will prove z < y.

We will prove PNoLt (SNoLev z) (λbeta ⇒ beta ∈ z) (SNoLev y) (λbeta ⇒ beta ∈ y).

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

We will prove PNoLt alpha (λbeta ⇒ beta ∈ z) (SNoLev y) (λbeta ⇒ beta ∈ y).

Apply PNoLtI2 to the current goal.

We will prove alpha ∈ SNoLev y.

An exact proof term for the current goal is Ha2.

We will prove PNoEq_ alpha (λbeta ⇒ beta ∈ z) (λbeta ⇒ beta ∈ y).

An exact proof term for the current goal is L5.

We will prove alpha ∈ y.

An exact proof term for the current goal is H4.

We will prove SNoLev z ∉ x.

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

An exact proof term for the current goal is H3.

We will prove SNoLev z ∈ y.

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

An exact proof term for the current goal is H4.

Assume H1: SNoLev x ∈ SNoLev y.

Assume H2: PNoEq_ (SNoLev x) (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y).

Assume H3: SNoLev x ∈ y.

Apply Hp2 to the current goal.

We will prove SNoLev x ∈ SNoLev y.

An exact proof term for the current goal is H1.

We will prove SNoEq_ (SNoLev x) x y.

An exact proof term for the current goal is H2.

We will prove SNoLev x ∈ y.

An exact proof term for the current goal is H3.

Assume H1: SNoLev y ∈ SNoLev x.

Assume H2: PNoEq_ (SNoLev y) (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y).

Assume H3: SNoLev y ∉ x.

Apply Hp3 to the current goal.

We will prove SNoLev y ∈ SNoLev x.

An exact proof term for the current goal is H1.

We will prove SNoEq_ (SNoLev y) x y.

An exact proof term for the current goal is H2.

We will prove SNoLev y ∉ x.

An exact proof term for the current goal is H3.