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

Assume Ha Hb.

Assume H1: PNo_upc R α p.

Assume H2: PNoLe α p β q.

We will prove PNo_upc R β 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: R γ r.

Assume H4: PNoLe γ r α p.

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

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 γ α β Hc Ha Hb r p q H4 H2.

∎