Let R, alpha, beta, p and q be given.

Assume Ha Hb.

Assume H1: PNo_upc R alpha p.

Assume H2: PNoLe alpha p beta q.

We will prove PNo_upc R beta q.

Apply H1 to the current goal.

Let gamma be given.

Assume H3.

Apply H3 to the current goal.

Assume Hc: ordinal gamma.

Assume H3.

Apply H3 to the current goal.

Let r be given.

Assume H3.

Apply H3 to the current goal.

Assume H3: R gamma r.

Assume H4: PNoLe gamma r alpha p.

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

We use gamma 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 gamma alpha beta Hc Ha Hb r p q H4 H2.

∎