Let L, α, β, p and q be given.

Assume Ha Hb.

Assume H1: PNo_downc L α p.

Assume H2: PNoLe β q α p.

We will prove PNo_downc L β q.

Apply H1 to the current goal.

Let γ be given.

Assume H3.

Apply H3 to the current goal.

Assume Hc: ordinal γ.

Assume H3.

Apply H3 to the current goal.

Let r be given.

Assume H3.

Apply H3 to the current goal.

Assume H3: L γ r.

Assume H4: PNoLe α p γ r.

We will prove ∃δ, ordinal δ ∧ ∃r : set → prop, L δ r ∧ PNoLe β q δ r.

We use γ to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hc.

We use r to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is PNoLe_tra β α γ Hb Ha Hc q p r H2 H4.

∎