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