Let x and y be given.
Assume Hx Hy.
Assume H1: PNoLe (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev y) (λbeta ⇒ beta ∈ y).
Apply H1 to the current goal.
Assume H2: PNoLt (SNoLev x) (λbeta ⇒ beta ∈ x) (SNoLev y) (λbeta ⇒ beta ∈ 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) (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y).
Apply orIR to the current goal.
An exact proof term for the current goal is SNo_eq x y Hx Hy H2 H3.
∎