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) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y) (λβ ⇒ β ∈ z) Hxy Hyz.