Let x and y be given.
Assume Hx Hy H1 H2.
Apply SNoLev_ x Hx to the current goal.
Assume Hx2a: x ⊆ SNoElts_ (SNoLev x).
Assume Hx2b: ∀beta ∈ SNoLev x, exactly1of2 (beta ' ∈ x) (beta ∈ x).
Apply SNoLev_ y Hy to the current goal.
Assume Hy2a: y ⊆ SNoElts_ (SNoLev y).
Assume Hy2b: ∀beta ∈ SNoLev y, exactly1of2 (beta ' ∈ y) (beta ∈ y).
Let u be given.
Assume Hu: u ∈ x.
We prove the intermediate claim L1: u ∈ SNoLev x ∪ {beta '|beta ∈ SNoLev x}.
An exact proof term for the current goal is Hx2a u Hu.
Apply binunionE (SNoLev x) {beta '|beta ∈ SNoLev x} u L1 to the current goal.
Assume H3: u ∈ SNoLev x.
Apply H2 u H3 to the current goal.
Assume H4 _.
An exact proof term for the current goal is H4 Hu.
Assume H3: u ∈ {beta '|beta ∈ SNoLev x}.
Apply ReplE_impred (SNoLev x) (λgamma ⇒ gamma ') u H3 to the current goal.
Let beta be given.
Assume H4: beta ∈ SNoLev x.
Assume H5: u = beta '.
We prove the intermediate claim L3: beta ∈ SNoLev y.
An exact proof term for the current goal is H1 beta H4.
Apply exactly1of2_E (beta ' ∈ y) (beta ∈ y) (Hy2b beta L3) to the current goal.
Assume H6: beta ' ∈ y.
Assume H7: beta ∉ y.
We will prove u ∈ y.
rewrite the current goal using H5 (from left to right).
An exact proof term for the current goal is H6.
Assume H6: beta ' ∉ y.
Assume H7: beta ∈ y.
We will prove False.
Apply exactly1of2_E (beta ' ∈ x) (beta ∈ x) (Hx2b beta H4) to the current goal.
Assume H8: beta ' ∈ x.
Assume H9: beta ∉ x.
Apply H9 to the current goal.
Apply H2 beta H4 to the current goal.
Assume _ H10.
An exact proof term for the current goal is H10 H7.
Assume H8: beta ' ∉ x.
Assume H9: beta ∈ x.
Apply H8 to the current goal.
We will prove beta ' ∈ x.
rewrite the current goal using H5 (from right to left).
An exact proof term for the current goal is Hu.
∎