An exact proof term for the current goal is PNoLt_irref (SNoLev x) (λbeta ⇒ beta ∈ x).