Let alpha, beta, p and q be given.

Assume Ha Hb.

We will prove PNoLt (SNoLev (PSNo alpha p)) (λgamma ⇒ gamma ∈ PSNo alpha p) (SNoLev (PSNo beta q)) (λgamma ⇒ gamma ∈ PSNo beta q) → PNoLt alpha p beta q.

rewrite the current goal using SNoLev_PSNo alpha Ha p (from left to right).

rewrite the current goal using SNoLev_PSNo beta Hb q (from left to right).

Assume H1: PNoLt alpha (λgamma ⇒ gamma ∈ PSNo alpha p) beta (λgamma ⇒ gamma ∈ PSNo beta q).

Apply PNoEqLt_tra alpha beta Ha Hb p (λgamma ⇒ gamma ∈ PSNo alpha p) q to the current goal.

We will prove PNoEq_ alpha p (λgamma ⇒ gamma ∈ PSNo alpha p).

Apply PNoEq_sym_ to the current goal.

Apply PNoEq_PSNo to the current goal.

An exact proof term for the current goal is Ha.

We will prove PNoLt alpha (λgamma ⇒ gamma ∈ PSNo alpha p) beta q.

Apply PNoLtEq_tra alpha beta Ha Hb (λgamma ⇒ gamma ∈ PSNo alpha p) (λgamma ⇒ gamma ∈ PSNo beta q) q to the current goal.

An exact proof term for the current goal is H1.

We will prove PNoEq_ beta (λgamma ⇒ gamma ∈ PSNo beta q) q.

Apply PNoEq_PSNo to the current goal.

An exact proof term for the current goal is Hb.

∎