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