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

An exact proof term for the current goal is binintersect_Subq_2 x (SNoElts_ alpha).

Let beta be given.

Assume Hb: beta ∈ alpha.

We prove the intermediate claim Lb: beta ∈ SNoLev x.

An exact proof term for the current goal is ordinal_TransSet (SNoLev x) (SNoLev_ordinal x Hx) alpha Ha beta Hb.

Apply exactly1of2_E (SetAdjoin beta {1} ∈ x) (beta ∈ x) (Hx2 beta Lb) to the current goal.

Assume H1: SetAdjoin beta {1} ∈ x.

Assume H2: beta ∉ x.

Apply exactly1of2_I1 to the current goal.

Apply binintersectI to the current goal.

An exact proof term for the current goal is H1.

We will prove SetAdjoin beta {1} ∈ SNoElts_ alpha.

We will prove SetAdjoin beta {1} ∈ alpha ∪ {SetAdjoin beta {1}|beta ∈ alpha}.

Apply binunionI2 to the current goal.

An exact proof term for the current goal is ReplI alpha (λbeta ⇒ SetAdjoin beta {1}) beta Hb.

We will prove beta ∉ x ∩ SNoElts_ alpha.

Assume H3.

An exact proof term for the current goal is H2 (binintersectE1 x (SNoElts_ alpha) beta H3).

Assume H1: SetAdjoin beta {1} ∉ x.

Assume H2: beta ∈ x.

Apply exactly1of2_I2 to the current goal.

Assume H3: SetAdjoin beta {1} ∈ x ∩ SNoElts_ alpha.

An exact proof term for the current goal is H1 (binintersectE1 x (SNoElts_ alpha) (SetAdjoin beta {1}) H3).

Apply binintersectI to the current goal.

An exact proof term for the current goal is H2.

We will prove beta ∈ SNoElts_ alpha.

We will prove beta ∈ alpha ∪ {SetAdjoin beta {1}|beta ∈ alpha}.

Apply binunionI1 to the current goal.

An exact proof term for the current goal is Hb.