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