Let α, β, p and q be given.
Assume Ha Hb.
We will prove PNoLt (SNoLev (PSNo α p)) (λγ ⇒ γ ∈ PSNo α p) (SNoLev (PSNo β q)) (λγ ⇒ γ ∈ PSNo β q) → PNoLt α p β q.
rewrite the current goal using SNoLev_PSNo α Ha p (from left to right).
rewrite the current goal using SNoLev_PSNo β Hb q (from left to right).
Assume H1: PNoLt α (λγ ⇒ γ ∈ PSNo α p) β (λγ ⇒ γ ∈ PSNo β q).
Apply PNoEqLt_tra α β Ha Hb p (λγ ⇒ γ ∈ PSNo α p) q to the current goal.
We will prove PNoEq_ α p (λγ ⇒ γ ∈ PSNo α 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 α (λγ ⇒ γ ∈ PSNo α p) β q.
Apply PNoLtEq_tra α β Ha Hb (λγ ⇒ γ ∈ PSNo α p) (λγ ⇒ γ ∈ PSNo β q) q to the current goal.
An exact proof term for the current goal is H1.
We will prove PNoEq_ β (λγ ⇒ γ ∈ PSNo β q) q.
Apply PNoEq_PSNo to the current goal.
An exact proof term for the current goal is Hb.
∎