Let R and α be given.

Assume Ha.

Let p be given.

Assume H1: R α p.

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

We use α to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Ha.

We use p to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H1.

Apply PNoLe_ref to the current goal.

∎