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