An exact proof term for the current goal is Sep_Subq (SNoS_ (SNoLev z)) (λx ⇒ x < z).