Let x and y be given.

Assume H1.

We will prove PNoLe (SNoLev x) (λβ ⇒ β ∈ x) (SNoLev y) (λβ ⇒ β ∈ y).

Apply PNoLeI1 to the current goal.

An exact proof term for the current goal is H1.

∎