Let x and y be given.

Assume Hx Hy Hxy Hyx.

Apply PNoLe_antisym (SNoLev x) (SNoLev y) (SNoLev_ordinal x Hx) (SNoLev_ordinal y Hy) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y) Hxy Hyx to the current goal.

Assume H1: SNoLev x = SNoLev y.

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

An exact proof term for the current goal is SNo_eq x y Hx Hy H1 H2.

∎