An exact proof term for the current goal is PNoLeLt_tra (SNoLev x) (SNoLev y) (SNoLev z) (SNoLev_ordinal x Hx) (SNoLev_ordinal y Hy) (SNoLev_ordinal z Hz) (λbeta ⇒ beta ∈ x) (λbeta ⇒ beta ∈ y) (λbeta ⇒ beta ∈ z) Hxy Hyz.