Let x and y be given.

Assume H1.

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

Apply PNoLeI1 to the current goal.

An exact proof term for the current goal is H1.

∎