Let x and y be given.
Assume Hx Hy.
Apply PNoLt_trichotomy_or (SNoLev x) (SNoLev y) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y) (SNoLev_ordinal x Hx) (SNoLev_ordinal y Hy) to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply or3I1 to the current goal.
An exact proof term for the current goal is H1.
Assume H1.
Apply H1 to the current goal.
Assume H2: SNoLev x = SNoLev y.
Assume H3: PNoEq_ (SNoLev x) (λβ ⇒ β ∈ x) (λβ ⇒ β ∈ y).
Apply or3I2 to the current goal.
An exact proof term for the current goal is SNo_eq x y Hx Hy H2 H3.
Assume H1.
Apply or3I3 to the current goal.
An exact proof term for the current goal is H1.
∎