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