Let x and y be given.

Assume Hx Hy.

Assume H1: PNoLe (SNoLev x) (λβ ⇒ β ∈ x) (SNoLev y) (λβ ⇒ β ∈ y).

Apply H1 to the current goal.

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

Apply orIL to the current goal.

An exact proof term for the current goal is H2.

Assume H2.

Apply H2 to the current goal.

Assume H2: SNoLev x = SNoLev y.

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

Apply orIR to the current goal.

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

∎